Theorem dfac5lem4 8949

Description: Lemma for dfac5 8951. (Contributed by NM, 11-Apr-2004.)

Hypotheses

Ref	Expression
dfac5lem.1	|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
dfac5lem.2	|- B = ( U. A i^i y )
dfac5lem.3	|- ( ph <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )

Assertion

Ref	Expression
dfac5lem4	|- ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )

Distinct variable groups:   x, z, y, w, v, u, t, h   z, B, w   x, A, y, z, w

Allowed substitution hints:   ph( x, y, z, w, v, u, t, h)   A( v, u, t, h)   B( x, y, v, u, t, h)

Proof of Theorem dfac5lem4

Dummy variable g is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3203	. . . . . 6 |- z e. _V
2		neeq1 2856	. . . . . . 7 |- ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
3		eqeq1 2626	. . . . . . . 8 |- ( u = z -> ( u = ( { t } X. t ) <-> z = ( { t } X. t ) ) )
4	3	rexbidv 3052	. . . . . . 7 |- ( u = z -> ( E. t e. h u = ( { t } X. t ) <-> E. t e. h z = ( { t } X. t ) ) )
5	2, 4	anbi12d 747	. . . . . 6 |- ( u = z -> ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) ) )
6	1, 5	elab 3350	. . . . 5 |- ( z e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) )
7	6	simplbi 476	. . . 4 |- ( z e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } -> z =/= (/) )
8		dfac5lem.1	. . . 4 |- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
9	7, 8	eleq2s 2719	. . 3 |- ( z e. A -> z =/= (/) )
10	9	rgen 2922	. 2 |- A. z e. A z =/= (/)
11		df-an 386	. . . . . . 7 |- ( ( x e. z /\ x e. w ) <-> -. ( x e. z -> -. x e. w ) )
12	1, 5, 8	elab2 3354	. . . . . . . . 9 |- ( z e. A <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) )
13	12	simprbi 480	. . . . . . . 8 |- ( z e. A -> E. t e. h z = ( { t } X. t ) )
14		vex 3203	. . . . . . . . . . 11 |- w e. _V
15		neeq1 2856	. . . . . . . . . . . 12 |- ( u = w -> ( u =/= (/) <-> w =/= (/) ) )
16		eqeq1 2626	. . . . . . . . . . . . 13 |- ( u = w -> ( u = ( { t } X. t ) <-> w = ( { t } X. t ) ) )
17	16	rexbidv 3052	. . . . . . . . . . . 12 |- ( u = w -> ( E. t e. h u = ( { t } X. t ) <-> E. t e. h w = ( { t } X. t ) ) )
18	15, 17	anbi12d 747	. . . . . . . . . . 11 |- ( u = w -> ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) <-> ( w =/= (/) /\ E. t e. h w = ( { t } X. t ) ) ) )
19	14, 18, 8	elab2 3354	. . . . . . . . . 10 |- ( w e. A <-> ( w =/= (/) /\ E. t e. h w = ( { t } X. t ) ) )
20	19	simprbi 480	. . . . . . . . 9 |- ( w e. A -> E. t e. h w = ( { t } X. t ) )
21		sneq 4187	. . . . . . . . . . . . 13 |- ( t = g -> { t } = { g } )
22	21	xpeq1d 5138	. . . . . . . . . . . 12 |- ( t = g -> ( { t } X. t ) = ( { g } X. t ) )
23		xpeq2 5129	. . . . . . . . . . . 12 |- ( t = g -> ( { g } X. t ) = ( { g } X. g ) )
24	22, 23	eqtrd 2656	. . . . . . . . . . 11 |- ( t = g -> ( { t } X. t ) = ( { g } X. g ) )
25	24	eqeq2d 2632	. . . . . . . . . 10 |- ( t = g -> ( w = ( { t } X. t ) <-> w = ( { g } X. g ) ) )
26	25	cbvrexv 3172	. . . . . . . . 9 |- ( E. t e. h w = ( { t } X. t ) <-> E. g e. h w = ( { g } X. g ) )
27	20, 26	sylib 208	. . . . . . . 8 |- ( w e. A -> E. g e. h w = ( { g } X. g ) )
28		eleq2 2690	. . . . . . . . . . . . . . . . . 18 |- ( z = ( { t } X. t ) -> ( x e. z <-> x e. ( { t } X. t ) ) )
29		elxp 5131	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( { t } X. t ) <-> E. u E. v ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) )
30		excom 2042	. . . . . . . . . . . . . . . . . . 19 |- ( E. u E. v ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) <-> E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) )
31	29, 30	bitri 264	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( { t } X. t ) <-> E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) )
32	28, 31	syl6bb 276	. . . . . . . . . . . . . . . . 17 |- ( z = ( { t } X. t ) -> ( x e. z <-> E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) ) )
33		eleq2 2690	. . . . . . . . . . . . . . . . . 18 |- ( w = ( { g } X. g ) -> ( x e. w <-> x e. ( { g } X. g ) ) )
34		elxp 5131	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( { g } X. g ) <-> E. u E. y ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) )
35		excom 2042	. . . . . . . . . . . . . . . . . . 19 |- ( E. u E. y ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) <-> E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) )
36	34, 35	bitri 264	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( { g } X. g ) <-> E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) )
37	33, 36	syl6bb 276	. . . . . . . . . . . . . . . . 17 |- ( w = ( { g } X. g ) -> ( x e. w <-> E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) )
38	32, 37	bi2anan9 917	. . . . . . . . . . . . . . . 16 |- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) <-> ( E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) ) )
39		eeanv 2182	. . . . . . . . . . . . . . . 16 |- ( E. v E. y ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) <-> ( E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) )
40	38, 39	syl6bbr 278	. . . . . . . . . . . . . . 15 |- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) <-> E. v E. y ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) ) )
41		velsn 4193	. . . . . . . . . . . . . . . . . . . . 21 |- ( u e. { t } <-> u = t )
42		opeq1 4402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = t -> <. u , v >. = <. t , v >. )
43	42	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = t -> ( x = <. u , v >. <-> x = <. t , v >. ) )
44	43	biimpac 503	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = <. u , v >. /\ u = t ) -> x = <. t , v >. )
45	41, 44	sylan2b 492	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = <. u , v >. /\ u e. { t } ) -> x = <. t , v >. )
46	45	adantrr 753	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) -> x = <. t , v >. )
47	46	exlimiv 1858	. . . . . . . . . . . . . . . . . 18 |- ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) -> x = <. t , v >. )
48		velsn 4193	. . . . . . . . . . . . . . . . . . . . 21 |- ( u e. { g } <-> u = g )
49		opeq1 4402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = g -> <. u , y >. = <. g , y >. )
50	49	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = g -> ( x = <. u , y >. <-> x = <. g , y >. ) )
51	50	biimpac 503	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = <. u , y >. /\ u = g ) -> x = <. g , y >. )
52	48, 51	sylan2b 492	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = <. u , y >. /\ u e. { g } ) -> x = <. g , y >. )
53	52	adantrr 753	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) -> x = <. g , y >. )
54	53	exlimiv 1858	. . . . . . . . . . . . . . . . . 18 |- ( E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) -> x = <. g , y >. )
55	47, 54	sylan9req 2677	. . . . . . . . . . . . . . . . 17 |- ( ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) -> <. t , v >. = <. g , y >. )
56		vex 3203	. . . . . . . . . . . . . . . . . 18 |- t e. _V
57		vex 3203	. . . . . . . . . . . . . . . . . 18 |- v e. _V
58	56, 57	opth1 4944	. . . . . . . . . . . . . . . . 17 |- ( <. t , v >. = <. g , y >. -> t = g )
59	55, 58	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) -> t = g )
60	59	exlimivv 1860	. . . . . . . . . . . . . . 15 |- ( E. v E. y ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) -> t = g )
61	40, 60	syl6bi 243	. . . . . . . . . . . . . 14 |- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> t = g ) )
62	61, 24	syl6 35	. . . . . . . . . . . . 13 |- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> ( { t } X. t ) = ( { g } X. g ) ) )
63		eqeq12 2635	. . . . . . . . . . . . 13 |- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( z = w <-> ( { t } X. t ) = ( { g } X. g ) ) )
64	62, 63	sylibrd 249	. . . . . . . . . . . 12 |- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
65	64	ex 450	. . . . . . . . . . 11 |- ( z = ( { t } X. t ) -> ( w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
66	65	rexlimivw 3029	. . . . . . . . . 10 |- ( E. t e. h z = ( { t } X. t ) -> ( w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
67	66	rexlimdvw 3034	. . . . . . . . 9 |- ( E. t e. h z = ( { t } X. t ) -> ( E. g e. h w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
68	67	imp 445	. . . . . . . 8 |- ( ( E. t e. h z = ( { t } X. t ) /\ E. g e. h w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
69	13, 27, 68	syl2an 494	. . . . . . 7 |- ( ( z e. A /\ w e. A ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
70	11, 69	syl5bir 233	. . . . . 6 |- ( ( z e. A /\ w e. A ) -> ( -. ( x e. z -> -. x e. w ) -> z = w ) )
71	70	necon1ad 2811	. . . . 5 |- ( ( z e. A /\ w e. A ) -> ( z =/= w -> ( x e. z -> -. x e. w ) ) )
72	71	alrimdv 1857	. . . 4 |- ( ( z e. A /\ w e. A ) -> ( z =/= w -> A. x ( x e. z -> -. x e. w ) ) )
73		disj1 4019	. . . 4 |- ( ( z i^i w ) = (/) <-> A. x ( x e. z -> -. x e. w ) )
74	72, 73	syl6ibr 242	. . 3 |- ( ( z e. A /\ w e. A ) -> ( z =/= w -> ( z i^i w ) = (/) ) )
75	74	rgen2a 2977	. 2 |- A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) )
76		dfac5lem.3	. . 3 |- ( ph <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
77		vex 3203	. . . . . . . 8 |- h e. _V
78		vuniex 6954	. . . . . . . 8 |- U. h e. _V
79	77, 78	xpex 6962	. . . . . . 7 |- ( h X. U. h ) e. _V
80	79	pwex 4848	. . . . . 6 |- ~P ( h X. U. h ) e. _V
81		snssi 4339	. . . . . . . . . . . 12 |- ( t e. h -> { t } C_ h )
82		elssuni 4467	. . . . . . . . . . . 12 |- ( t e. h -> t C_ U. h )
83		xpss12 5225	. . . . . . . . . . . 12 |- ( ( { t } C_ h /\ t C_ U. h ) -> ( { t } X. t ) C_ ( h X. U. h ) )
84	81, 82, 83	syl2anc 693	. . . . . . . . . . 11 |- ( t e. h -> ( { t } X. t ) C_ ( h X. U. h ) )
85		snex 4908	. . . . . . . . . . . . 13 |- { t } e. _V
86	85, 56	xpex 6962	. . . . . . . . . . . 12 |- ( { t } X. t ) e. _V
87	86	elpw 4164	. . . . . . . . . . 11 |- ( ( { t } X. t ) e. ~P ( h X. U. h ) <-> ( { t } X. t ) C_ ( h X. U. h ) )
88	84, 87	sylibr 224	. . . . . . . . . 10 |- ( t e. h -> ( { t } X. t ) e. ~P ( h X. U. h ) )
89		eleq1 2689	. . . . . . . . . 10 |- ( u = ( { t } X. t ) -> ( u e. ~P ( h X. U. h ) <-> ( { t } X. t ) e. ~P ( h X. U. h ) ) )
90	88, 89	syl5ibrcom 237	. . . . . . . . 9 |- ( t e. h -> ( u = ( { t } X. t ) -> u e. ~P ( h X. U. h ) ) )
91	90	rexlimiv 3027	. . . . . . . 8 |- ( E. t e. h u = ( { t } X. t ) -> u e. ~P ( h X. U. h ) )
92	91	adantl 482	. . . . . . 7 |- ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) -> u e. ~P ( h X. U. h ) )
93	92	abssi 3677	. . . . . 6 |- { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } C_ ~P ( h X. U. h )
94	80, 93	ssexi 4803	. . . . 5 |- { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } e. _V
95	8, 94	eqeltri 2697	. . . 4 |- A e. _V
96		raleq 3138	. . . . . 6 |- ( x = A -> ( A. z e. x z =/= (/) <-> A. z e. A z =/= (/) ) )
97		raleq 3138	. . . . . . 7 |- ( x = A -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) )
98	97	raleqbi1dv 3146	. . . . . 6 |- ( x = A -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) )
99	96, 98	anbi12d 747	. . . . 5 |- ( x = A -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( A. z e. A z =/= (/) /\ A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) ) )
100		raleq 3138	. . . . . 6 |- ( x = A -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. A E! v v e. ( z i^i y ) ) )
101	100	exbidv 1850	. . . . 5 |- ( x = A -> ( E. y A. z e. x E! v v e. ( z i^i y ) <-> E. y A. z e. A E! v v e. ( z i^i y ) ) )
102	99, 101	imbi12d 334	. . . 4 |- ( x = A -> ( ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> ( ( A. z e. A z =/= (/) /\ A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. A E! v v e. ( z i^i y ) ) ) )
103	95, 102	spcv 3299	. . 3 |- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> ( ( A. z e. A z =/= (/) /\ A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. A E! v v e. ( z i^i y ) ) )
104	76, 103	sylbi 207	. 2 |- ( ph -> ( ( A. z e. A z =/= (/) /\ A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. A E! v v e. ( z i^i y ) ) )
105	10, 75, 104	mp2ani 714	1 |- ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   E!weu 2470   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   <.cop 4183   U.cuni 4436   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  dfac5lem5  8950