Theorem ax11eq 1754

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

Assertion

Ref	Expression
ax11eq	|- (-. A.x x = y -> (x = y -> (z = w -> A.x(x = y -> z = w))))

Proof of Theorem ax11eq

Step	Hyp	Ref	Expression
1		19.26 1416	. . 3 |- (A.x(x = z /\ x = w) <-> (A.x x = z /\ A.x x = w))
2		equid 1484	. . . . . . . 8 |- x = x
3	2	a1i 8	. . . . . . 7 |- (x = y -> x = x)
4	3	ax-gen 1305	. . . . . 6 |- A.x(x = y -> x = x)
5	4	a1i 8	. . . . 5 |- (x = x -> A.x(x = y -> x = x))
6		equequ1 1494	. . . . . . . . 9 |- (x = z -> (x = x <-> z = x))
7		equequ2 1495	. . . . . . . . 9 |- (x = w -> (z = x <-> z = w))
8	6, 7	sylan9bb 599	. . . . . . . 8 |- ((x = z /\ x = w) -> (x = x <-> z = w))
9	8	a4s 1330	. . . . . . 7 |- (A.x(x = z /\ x = w) -> (x = x <-> z = w))
10		hba1 1350	. . . . . . . 8 |- (A.x(x = z /\ x = w) -> A.xA.x(x = z /\ x = w))
11	9	imbi2d 674	. . . . . . . 8 |- (A.x(x = z /\ x = w) -> ((x = y -> x = x) <-> (x = y -> z = w)))
12	10, 11	albid 1459	. . . . . . 7 |- (A.x(x = z /\ x = w) -> (A.x(x = y -> x = x) <-> A.x(x = y -> z = w)))
13	9, 12	imbi12d 688	. . . . . 6 |- (A.x(x = z /\ x = w) -> ((x = x -> A.x(x = y -> x = x)) <-> (z = w -> A.x(x = y -> z = w))))
14	13	adantr 425	. . . . 5 |- ((A.x(x = z /\ x = w) /\ (-. A.x x = y /\ x = y)) -> ((x = x -> A.x(x = y -> x = x)) <-> (z = w -> A.x(x = y -> z = w))))
15	5, 14	mpbii 210	. . . 4 |- ((A.x(x = z /\ x = w) /\ (-. A.x x = y /\ x = y)) -> (z = w -> A.x(x = y -> z = w)))
16	15	exp32 408	. . 3 |- (A.x(x = z /\ x = w) -> (-. A.x x = y -> (x = y -> (z = w -> A.x(x = y -> z = w)))))
17	1, 16	sylbir 218	. 2 |- ((A.x x = z /\ A.x x = w) -> (-. A.x x = y -> (x = y -> (z = w -> A.x(x = y -> z = w)))))
18		equequ1 1494	. . . . . . 7 |- (x = y -> (x = w <-> y = w))
19	18	ad2antll 443	. . . . . 6 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x = w <-> y = w))
20		ax-12 1310	. . . . . . . . 9 |- (-. A.x x = y -> (-. A.x x = w -> (y = w -> A.x y = w)))
21	20	impcom 378	. . . . . . . 8 |- ((-. A.x x = w /\ -. A.x x = y) -> (y = w -> A.x y = w))
22	21	adantrr 431	. . . . . . 7 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (y = w -> A.x y = w))
23		equtrr 1491	. . . . . . . 8 |- (y = w -> (x = y -> x = w))
24	23	alimi 1338	. . . . . . 7 |- (A.x y = w -> A.x(x = y -> x = w))
25	22, 24	syl6 25	. . . . . 6 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (y = w -> A.x(x = y -> x = w)))
26	19, 25	sylbid 220	. . . . 5 |- ((-. A.x x = w /\ (-. A.x x = y /\ x = y)) -> (x = w -> A.x(x = y -> x = w)))
27	26	adantll 428	. . . 4 |- (((A.x x = z /\ -. A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (x = w -> A.x(x = y -> x = w)))
28		equequ1 1494	. . . . . . 7 |- (x = z -> (x = w <-> z = w))
29	28	a4s 1330	. . . . . 6 |- (A.x x = z -> (x = w <-> z = w))
30	29	imbi2d 674	. . . . . . 7 |- (A.x x = z -> ((x = y -> x = w) <-> (x = y -> z = w)))
31	30	dral2 1516	. . . . . 6 |- (A.x x = z -> (A.x(x = y -> x = w) <-> A.x(x = y -> z = w)))
32	29, 31	imbi12d 688	. . . . 5 |- (A.x x = z -> ((x = w -> A.x(x = y -> x = w)) <-> (z = w -> A.x(x = y -> z = w))))
33	32	ad2antrr 440	. . . 4 |- (((A.x x = z /\ -. A.x x = w) /\ (-. A.x x = y /\ x = y)) -> ((x = w -> A.x(x = y -> x = w)) <-> (z = w -> A.x(x = y -> z = w))))
34	27, 33	mpbid 212	. . 3 |- (((A.x x = z /\ -. A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (z = w -> A.x(x = y -> z = w)))
35	34	exp32 408	. 2 |- ((A.x x = z /\ -. A.x x = w) -> (-. A.x x = y -> (x = y -> (z = w -> A.x(x = y -> z = w)))))
36		equequ2 1495	. . . . . . 7 |- (x = y -> (z = x <-> z = y))
37	36	ad2antll 443	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z = x <-> z = y))
38		ax-12 1310	. . . . . . . . 9 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
39	38	imp 377	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> (z = y -> A.x z = y))
40	39	adantrr 431	. . . . . . 7 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z = y -> A.x z = y))
41	36	biimprcd 173	. . . . . . . 8 |- (z = y -> (x = y -> z = x))
42	41	alimi 1338	. . . . . . 7 |- (A.x z = y -> A.x(x = y -> z = x))
43	40, 42	syl6 25	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z = y -> A.x(x = y -> z = x)))
44	37, 43	sylbid 220	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ x = y)) -> (z = x -> A.x(x = y -> z = x)))
45	44	adantlr 429	. . . 4 |- (((-. A.x x = z /\ A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (z = x -> A.x(x = y -> z = x)))
46	7	a4s 1330	. . . . . 6 |- (A.x x = w -> (z = x <-> z = w))
47	46	imbi2d 674	. . . . . . 7 |- (A.x x = w -> ((x = y -> z = x) <-> (x = y -> z = w)))
48	47	dral2 1516	. . . . . 6 |- (A.x x = w -> (A.x(x = y -> z = x) <-> A.x(x = y -> z = w)))
49	46, 48	imbi12d 688	. . . . 5 |- (A.x x = w -> ((z = x -> A.x(x = y -> z = x)) <-> (z = w -> A.x(x = y -> z = w))))
50	49	ad2antlr 441	. . . 4 |- (((-. A.x x = z /\ A.x x = w) /\ (-. A.x x = y /\ x = y)) -> ((z = x -> A.x(x = y -> z = x)) <-> (z = w -> A.x(x = y -> z = w))))
51	45, 50	mpbid 212	. . 3 |- (((-. A.x x = z /\ A.x x = w) /\ (-. A.x x = y /\ x = y)) -> (z = w -> A.x(x = y -> z = w)))
52	51	exp32 408	. 2 |- ((-. A.x x = z /\ A.x x = w) -> (-. A.x x = y -> (x = y -> (z = w -> A.x(x = y -> z = w)))))
53		a9e 1483	. . . . 5 |- E.u u = w
54		a9e 1483	. . . . . . 7 |- E.v v = z
55		ax-1 4	. . . . . . . . . . 11 |- (v = u -> (x = y -> v = u))
56	55	19.21aiv 1664	. . . . . . . . . 10 |- (v = u -> A.x(x = y -> v = u))
57		equequ1 1494	. . . . . . . . . . . . 13 |- (v = z -> (v = u <-> z = u))
58		equequ2 1495	. . . . . . . . . . . . 13 |- (u = w -> (z = u <-> z = w))
59	57, 58	sylan9bb 599	. . . . . . . . . . . 12 |- ((v = z /\ u = w) -> (v = u <-> z = w))
60	59	adantl 424	. . . . . . . . . . 11 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (v = u <-> z = w))
61		dveeq2 1582	. . . . . . . . . . . . . . 15 |- (-. A.x x = z -> (v = z -> A.x v = z))
62		dveeq2 1582	. . . . . . . . . . . . . . 15 |- (-. A.x x = w -> (u = w -> A.x u = w))
63	61, 62	im2anan9 622	. . . . . . . . . . . . . 14 |- ((-. A.x x = z /\ -. A.x x = w) -> ((v = z /\ u = w) -> (A.x v = z /\ A.x u = w)))
64	63	imp 377	. . . . . . . . . . . . 13 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (A.x v = z /\ A.x u = w))
65		19.26 1416	. . . . . . . . . . . . 13 |- (A.x(v = z /\ u = w) <-> (A.x v = z /\ A.x u = w))
66	64, 65	sylibr 217	. . . . . . . . . . . 12 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> A.x(v = z /\ u = w))
67		hba1 1350	. . . . . . . . . . . . 13 |- (A.x(v = z /\ u = w) -> A.xA.x(v = z /\ u = w))
68	59	a4s 1330	. . . . . . . . . . . . . 14 |- (A.x(v = z /\ u = w) -> (v = u <-> z = w))
69	68	imbi2d 674	. . . . . . . . . . . . 13 |- (A.x(v = z /\ u = w) -> ((x = y -> v = u) <-> (x = y -> z = w)))
70	67, 69	albid 1459	. . . . . . . . . . . 12 |- (A.x(v = z /\ u = w) -> (A.x(x = y -> v = u) <-> A.x(x = y -> z = w)))
71	66, 70	syl 12	. . . . . . . . . . 11 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (A.x(x = y -> v = u) <-> A.x(x = y -> z = w)))
72	60, 71	imbi12d 688	. . . . . . . . . 10 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> ((v = u -> A.x(x = y -> v = u)) <-> (z = w -> A.x(x = y -> z = w))))
73	56, 72	mpbii 210	. . . . . . . . 9 |- (((-. A.x x = z /\ -. A.x x = w) /\ (v = z /\ u = w)) -> (z = w -> A.x(x = y -> z = w)))
74	73	exp32 408	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = w) -> (v = z -> (u = w -> (z = w -> A.x(x = y -> z = w)))))
75	74	19.23adv 1584	. . . . . . 7 |- ((-. A.x x = z /\ -. A.x x = w) -> (E.v v = z -> (u = w -> (z = w -> A.x(x = y -> z = w)))))
76	54, 75	mpi 55	. . . . . 6 |- ((-. A.x x = z /\ -. A.x x = w) -> (u = w -> (z = w -> A.x(x = y -> z = w))))
77	76	19.23adv 1584	. . . . 5 |- ((-. A.x x = z /\ -. A.x x = w) -> (E.u u = w -> (z = w -> A.x(x = y -> z = w))))
78	53, 77	mpi 55	. . . 4 |- ((-. A.x x = z /\ -. A.x x = w) -> (z = w -> A.x(x = y -> z = w)))
79	78	a1d 15	. . 3 |- ((-. A.x x = z /\ -. A.x x = w) -> (x = y -> (z = w -> A.x(x = y -> z = w))))
80	79	a1d 15	. 2 |- ((-. A.x x = z /\ -. A.x x = w) -> (-. A.x x = y -> (x = y -> (z = w -> A.x(x = y -> z = w)))))
81	17, 35, 52, 80	4cases 832	1 |- (-. A.x x = y -> (x = y -> (z = w -> A.x(x = y -> z = w))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298  E.wex 1326

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain