Theorem ax11eq 1365

Description: Basis step for constructing a substitution instance of ax-11o 1220 without using ax-11o 1220. Atomic formula for equality predicate.

Assertion

Ref	Expression
ax11eq	⊢ (¬ ∀x x = y → (x = y → (z = w → ∀x(x = y → z = w))))

Proof of Theorem ax11eq

Step	Hyp	Ref	Expression
1		19.26 1069	. . 3 ⊢ (∀x(x = z ⋀ x = w) ↔ (∀x x = z ⋀ ∀x x = w))
2		equid 1128	. . . . . . . 8 ⊢ x = x
3	2	a1i 8	. . . . . . 7 ⊢ (x = y → x = x)
4	3	ax-gen 965	. . . . . 6 ⊢ ∀x(x = y → x = x)
5	4	a1i 8	. . . . 5 ⊢ (x = x → ∀x(x = y → x = x))
6		equequ1 1136	. . . . . . . . 9 ⊢ (x = z → (x = x ↔ z = x))
7		equequ2 1137	. . . . . . . . 9 ⊢ (x = w → (z = x ↔ z = w))
8	6, 7	sylan9bb 542	. . . . . . . 8 ⊢ ((x = z ⋀ x = w) → (x = x ↔ z = w))
9	8	a4s 986	. . . . . . 7 ⊢ (∀x(x = z ⋀ x = w) → (x = x ↔ z = w))
10		hba1 1005	. . . . . . . 8 ⊢ (∀x(x = z ⋀ x = w) → ∀x∀x(x = z ⋀ x = w))
11	9	imbi2d 614	. . . . . . . 8 ⊢ (∀x(x = z ⋀ x = w) → ((x = y → x = x) ↔ (x = y → z = w)))
12	10, 11	albid 1106	. . . . . . 7 ⊢ (∀x(x = z ⋀ x = w) → (∀x(x = y → x = x) ↔ ∀x(x = y → z = w)))
13	9, 12	imbi12d 628	. . . . . 6 ⊢ (∀x(x = z ⋀ x = w) → ((x = x → ∀x(x = y → x = x)) ↔ (z = w → ∀x(x = y → z = w))))
14	13	adantr 391	. . . . 5 ⊢ ((∀x(x = z ⋀ x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → ((x = x → ∀x(x = y → x = x)) ↔ (z = w → ∀x(x = y → z = w))))
15	5, 14	mpbii 193	. . . 4 ⊢ ((∀x(x = z ⋀ x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = w → ∀x(x = y → z = w)))
16	15	exp32 379	. . 3 ⊢ (∀x(x = z ⋀ x = w) → (¬ ∀x x = y → (x = y → (z = w → ∀x(x = y → z = w)))))
17	1, 16	sylbir 201	. 2 ⊢ ((∀x x = z ⋀ ∀x x = w) → (¬ ∀x x = y → (x = y → (z = w → ∀x(x = y → z = w)))))
18		equequ1 1136	. . . . . . 7 ⊢ (x = y → (x = w ↔ y = w))
19	18	ad2antll 409	. . . . . 6 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (x = w ↔ y = w))
20		ax-12 970	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (¬ ∀x x = w → (y = w → ∀x y = w)))
21	20	impcom 351	. . . . . . . 8 ⊢ ((¬ ∀x x = w ⋀ ¬ ∀x x = y) → (y = w → ∀x y = w))
22	21	adantrr 397	. . . . . . 7 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (y = w → ∀x y = w))
23		equtrr 1134	. . . . . . . 8 ⊢ (y = w → (x = y → x = w))
24	23	19.20i 994	. . . . . . 7 ⊢ (∀x y = w → ∀x(x = y → x = w))
25	22, 24	syl6 22	. . . . . 6 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (y = w → ∀x(x = y → x = w)))
26	19, 25	sylbid 203	. . . . 5 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (x = w → ∀x(x = y → x = w)))
27	26	adantll 394	. . . 4 ⊢ (((∀x x = z ⋀ ¬ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (x = w → ∀x(x = y → x = w)))
28		equequ1 1136	. . . . . . 7 ⊢ (x = z → (x = w ↔ z = w))
29	28	a4s 986	. . . . . 6 ⊢ (∀x x = z → (x = w ↔ z = w))
30	29	imbi2d 614	. . . . . . 7 ⊢ (∀x x = z → ((x = y → x = w) ↔ (x = y → z = w)))
31	30	dral2 1157	. . . . . 6 ⊢ (∀x x = z → (∀x(x = y → x = w) ↔ ∀x(x = y → z = w)))
32	29, 31	imbi12d 628	. . . . 5 ⊢ (∀x x = z → ((x = w → ∀x(x = y → x = w)) ↔ (z = w → ∀x(x = y → z = w))))
33	32	ad2antrr 406	. . . 4 ⊢ (((∀x x = z ⋀ ¬ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → ((x = w → ∀x(x = y → x = w)) ↔ (z = w → ∀x(x = y → z = w))))
34	27, 33	mpbid 195	. . 3 ⊢ (((∀x x = z ⋀ ¬ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = w → ∀x(x = y → z = w)))
35	34	exp32 379	. 2 ⊢ ((∀x x = z ⋀ ¬ ∀x x = w) → (¬ ∀x x = y → (x = y → (z = w → ∀x(x = y → z = w)))))
36		equequ2 1137	. . . . . . 7 ⊢ (x = y → (z = x ↔ z = y))
37	36	ad2antll 409	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = x ↔ z = y))
38		ax-12 970	. . . . . . . . 9 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z = y → ∀x z = y)))
39	38	imp 350	. . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (z = y → ∀x z = y))
40	39	adantrr 397	. . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = y → ∀x z = y))
41	36	biimprcd 156	. . . . . . . 8 ⊢ (z = y → (x = y → z = x))
42	41	19.20i 994	. . . . . . 7 ⊢ (∀x z = y → ∀x(x = y → z = x))
43	40, 42	syl6 22	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = y → ∀x(x = y → z = x)))
44	37, 43	sylbid 203	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = x → ∀x(x = y → z = x)))
45	44	adantlr 395	. . . 4 ⊢ (((¬ ∀x x = z ⋀ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = x → ∀x(x = y → z = x)))
46	7	a4s 986	. . . . . 6 ⊢ (∀x x = w → (z = x ↔ z = w))
47	46	imbi2d 614	. . . . . . 7 ⊢ (∀x x = w → ((x = y → z = x) ↔ (x = y → z = w)))
48	47	dral2 1157	. . . . . 6 ⊢ (∀x x = w → (∀x(x = y → z = x) ↔ ∀x(x = y → z = w)))
49	46, 48	imbi12d 628	. . . . 5 ⊢ (∀x x = w → ((z = x → ∀x(x = y → z = x)) ↔ (z = w → ∀x(x = y → z = w))))
50	49	ad2antlr 407	. . . 4 ⊢ (((¬ ∀x x = z ⋀ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → ((z = x → ∀x(x = y → z = x)) ↔ (z = w → ∀x(x = y → z = w))))
51	45, 50	mpbid 195	. . 3 ⊢ (((¬ ∀x x = z ⋀ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z = w → ∀x(x = y → z = w)))
52	51	exp32 379	. 2 ⊢ ((¬ ∀x x = z ⋀ ∀x x = w) → (¬ ∀x x = y → (x = y → (z = w → ∀x(x = y → z = w)))))
53		a9e 1127	. . . . 5 ⊢ ∃u u = w
54		a9e 1127	. . . . . . 7 ⊢ ∃v v = z
55		ax-1 4	. . . . . . . . . . 11 ⊢ (v = u → (x = y → v = u))
56	55	19.21aiv 1288	. . . . . . . . . 10 ⊢ (v = u → ∀x(x = y → v = u))
57		equequ1 1136	. . . . . . . . . . . . 13 ⊢ (v = z → (v = u ↔ z = u))
58		equequ2 1137	. . . . . . . . . . . . 13 ⊢ (u = w → (z = u ↔ z = w))
59	57, 58	sylan9bb 542	. . . . . . . . . . . 12 ⊢ ((v = z ⋀ u = w) → (v = u ↔ z = w))
60	59	adantl 390	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → (v = u ↔ z = w))
61		dveeq2 1214	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = z → (v = z → ∀x v = z))
62		dveeq2 1214	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = w → (u = w → ∀x u = w))
63	61, 62	im2anan9 565	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → ((v = z ⋀ u = w) → (∀x v = z ⋀ ∀x u = w)))
64	63	imp 350	. . . . . . . . . . . . 13 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → (∀x v = z ⋀ ∀x u = w))
65		19.26 1069	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ⋀ u = w) ↔ (∀x v = z ⋀ ∀x u = w))
66	64, 65	sylibr 200	. . . . . . . . . . . 12 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → ∀x(v = z ⋀ u = w))
67		hba1 1005	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ⋀ u = w) → ∀x∀x(v = z ⋀ u = w))
68	59	a4s 986	. . . . . . . . . . . . . 14 ⊢ (∀x(v = z ⋀ u = w) → (v = u ↔ z = w))
69	68	imbi2d 614	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ⋀ u = w) → ((x = y → v = u) ↔ (x = y → z = w)))
70	67, 69	albid 1106	. . . . . . . . . . . 12 ⊢ (∀x(v = z ⋀ u = w) → (∀x(x = y → v = u) ↔ ∀x(x = y → z = w)))
71	66, 70	syl 10	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → (∀x(x = y → v = u) ↔ ∀x(x = y → z = w)))
72	60, 71	imbi12d 628	. . . . . . . . . 10 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → ((v = u → ∀x(x = y → v = u)) ↔ (z = w → ∀x(x = y → z = w))))
73	56, 72	mpbii 193	. . . . . . . . 9 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → (z = w → ∀x(x = y → z = w)))
74	73	exp32 379	. . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (v = z → (u = w → (z = w → ∀x(x = y → z = w)))))
75	74	19.23adv 1216	. . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (∃v v = z → (u = w → (z = w → ∀x(x = y → z = w)))))
76	54, 75	mpi 44	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (u = w → (z = w → ∀x(x = y → z = w))))
77	76	19.23adv 1216	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (∃u u = w → (z = w → ∀x(x = y → z = w))))
78	53, 77	mpi 44	. . . 4 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (z = w → ∀x(x = y → z = w)))
79	78	a1d 12	. . 3 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (x = y → (z = w → ∀x(x = y → z = w))))
80	79	a1d 12	. 2 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (¬ ∀x x = y → (x = y → (z = w → ∀x(x = y → z = w)))))
81	17, 35, 52, 80	4cases 760	1 ⊢ (¬ ∀x x = y → (x = y → (z = w → ∀x(x = y → z = w))))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 956   = wceq 958  ∃wex 982

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983

Copyright terms: Public domain