Theorem dfac5lem4OLD

Description: Obsolete version of dfac5lem4 as of 23-Jun-2025. (Contributed by NM, 11-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dfac5lem.1	|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
	dfac5lemOLD.2	|- B = ( U. A i^i y )
	dfac5lemOLD.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	dfac5lem4OLD	|- ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )

Proof

Step	Hyp	Ref	Expression
1		dfac5lem.1	|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
2		dfac5lemOLD.2	|- B = ( U. A i^i y )
3		dfac5lemOLD.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 ) ) )
4		vex	|- z e. _V
5		neeq1	|- ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
6		eqeq1	|- ( u = z -> ( u = ( { t } X. t ) <-> z = ( { t } X. t ) ) )
7	6	rexbidv	|- ( u = z -> ( E. t e. h u = ( { t } X. t ) <-> E. t e. h z = ( { t } X. t ) ) )
8	5 7	anbi12d	|- ( u = z -> ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) ) )
9	4 8	elab	|- ( z e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) )
10	9	simplbi	|- ( z e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } -> z =/= (/) )
11	10 1	eleq2s	|- ( z e. A -> z =/= (/) )
12	11	rgen	|- A. z e. A z =/= (/)
13		df-an	|- ( ( x e. z /\ x e. w ) <-> -. ( x e. z -> -. x e. w ) )
14	4 8 1	elab2	|- ( z e. A <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) )
15	14	simprbi	|- ( z e. A -> E. t e. h z = ( { t } X. t ) )
16		vex	|- w e. _V
17		neeq1	|- ( u = w -> ( u =/= (/) <-> w =/= (/) ) )
18		eqeq1	|- ( u = w -> ( u = ( { t } X. t ) <-> w = ( { t } X. t ) ) )
19	18	rexbidv	|- ( u = w -> ( E. t e. h u = ( { t } X. t ) <-> E. t e. h w = ( { t } X. t ) ) )
20	17 19	anbi12d	|- ( u = w -> ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) <-> ( w =/= (/) /\ E. t e. h w = ( { t } X. t ) ) ) )
21	16 20 1	elab2	|- ( w e. A <-> ( w =/= (/) /\ E. t e. h w = ( { t } X. t ) ) )
22	21	simprbi	|- ( w e. A -> E. t e. h w = ( { t } X. t ) )
23		sneq	|- ( t = g -> { t } = { g } )
24	23	xpeq1d	|- ( t = g -> ( { t } X. t ) = ( { g } X. t ) )
25		xpeq2	|- ( t = g -> ( { g } X. t ) = ( { g } X. g ) )
26	24 25	eqtrd	|- ( t = g -> ( { t } X. t ) = ( { g } X. g ) )
27	26	eqeq2d	|- ( t = g -> ( w = ( { t } X. t ) <-> w = ( { g } X. g ) ) )
28	27	cbvrexvw	|- ( E. t e. h w = ( { t } X. t ) <-> E. g e. h w = ( { g } X. g ) )
29	22 28	sylib	|- ( w e. A -> E. g e. h w = ( { g } X. g ) )
30		eleq2	|- ( z = ( { t } X. t ) -> ( x e. z <-> x e. ( { t } X. t ) ) )
31		elxp	|- ( x e. ( { t } X. t ) <-> E. u E. v ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) )
32		excom	|- ( 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 ) ) )
33	31 32	bitri	|- ( x e. ( { t } X. t ) <-> E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) )
34	30 33	bitrdi	|- ( z = ( { t } X. t ) -> ( x e. z <-> E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) ) )
35		eleq2	|- ( w = ( { g } X. g ) -> ( x e. w <-> x e. ( { g } X. g ) ) )
36		elxp	|- ( x e. ( { g } X. g ) <-> E. u E. y ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) )
37		excom	|- ( 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 ) ) )
38	36 37	bitri	|- ( x e. ( { g } X. g ) <-> E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) )
39	35 38	bitrdi	|- ( w = ( { g } X. g ) -> ( x e. w <-> E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) )
40	34 39	bi2anan9	|- ( ( 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 ) ) ) ) )
41		exdistrv	|- ( 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 ) ) ) )
42	40 41	bitr4di	|- ( ( 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 ) ) ) ) )
43		velsn	|- ( u e. { t } <-> u = t )
44		opeq1	|- ( u = t -> <. u , v >. = <. t , v >. )
45	44	eqeq2d	|- ( u = t -> ( x = <. u , v >. <-> x = <. t , v >. ) )
46	45	biimpac	|- ( ( x = <. u , v >. /\ u = t ) -> x = <. t , v >. )
47	43 46	sylan2b	|- ( ( x = <. u , v >. /\ u e. { t } ) -> x = <. t , v >. )
48	47	adantrr	|- ( ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) -> x = <. t , v >. )
49	48	exlimiv	|- ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) -> x = <. t , v >. )
50		velsn	|- ( u e. { g } <-> u = g )
51		opeq1	|- ( u = g -> <. u , y >. = <. g , y >. )
52	51	eqeq2d	|- ( u = g -> ( x = <. u , y >. <-> x = <. g , y >. ) )
53	52	biimpac	|- ( ( x = <. u , y >. /\ u = g ) -> x = <. g , y >. )
54	50 53	sylan2b	|- ( ( x = <. u , y >. /\ u e. { g } ) -> x = <. g , y >. )
55	54	adantrr	|- ( ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) -> x = <. g , y >. )
56	55	exlimiv	|- ( E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) -> x = <. g , y >. )
57	49 56	sylan9req	|- ( ( 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 >. )
58		vex	|- t e. _V
59		vex	|- v e. _V
60	58 59	opth1	|- ( <. t , v >. = <. g , y >. -> t = g )
61	57 60	syl	|- ( ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) /\ E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) -> t = g )
62	61	exlimivv	|- ( 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 )
63	42 62	biimtrdi	|- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> t = g ) )
64	63 26	syl6	|- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> ( { t } X. t ) = ( { g } X. g ) ) )
65		eqeq12	|- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( z = w <-> ( { t } X. t ) = ( { g } X. g ) ) )
66	64 65	sylibrd	|- ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
67	66	ex	|- ( z = ( { t } X. t ) -> ( w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
68	67	rexlimivw	|- ( E. t e. h z = ( { t } X. t ) -> ( w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
69	68	rexlimdvw	|- ( E. t e. h z = ( { t } X. t ) -> ( E. g e. h w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
70	69	imp	|- ( ( E. t e. h z = ( { t } X. t ) /\ E. g e. h w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
71	15 29 70	syl2an	|- ( ( z e. A /\ w e. A ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
72	13 71	biimtrrid	|- ( ( z e. A /\ w e. A ) -> ( -. ( x e. z -> -. x e. w ) -> z = w ) )
73	72	necon1ad	|- ( ( z e. A /\ w e. A ) -> ( z =/= w -> ( x e. z -> -. x e. w ) ) )
74	73	alrimdv	|- ( ( z e. A /\ w e. A ) -> ( z =/= w -> A. x ( x e. z -> -. x e. w ) ) )
75		disj1	|- ( ( z i^i w ) = (/) <-> A. x ( x e. z -> -. x e. w ) )
76	74 75	imbitrrdi	|- ( ( z e. A /\ w e. A ) -> ( z =/= w -> ( z i^i w ) = (/) ) )
77	76	rgen2	|- A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) )
78		vex	|- h e. _V
79		vuniex	|- U. h e. _V
80	78 79	xpex	|- ( h X. U. h ) e. _V
81	80	pwex	|- ~P ( h X. U. h ) e. _V
82		snssi	|- ( t e. h -> { t } C_ h )
83		elssuni	|- ( t e. h -> t C_ U. h )
84		xpss12	|- ( ( { t } C_ h /\ t C_ U. h ) -> ( { t } X. t ) C_ ( h X. U. h ) )
85	82 83 84	syl2anc	|- ( t e. h -> ( { t } X. t ) C_ ( h X. U. h ) )
86		vsnex	|- { t } e. _V
87	86 58	xpex	|- ( { t } X. t ) e. _V
88	87	elpw	|- ( ( { t } X. t ) e. ~P ( h X. U. h ) <-> ( { t } X. t ) C_ ( h X. U. h ) )
89	85 88	sylibr	|- ( t e. h -> ( { t } X. t ) e. ~P ( h X. U. h ) )
90		eleq1	|- ( u = ( { t } X. t ) -> ( u e. ~P ( h X. U. h ) <-> ( { t } X. t ) e. ~P ( h X. U. h ) ) )
91	89 90	syl5ibrcom	|- ( t e. h -> ( u = ( { t } X. t ) -> u e. ~P ( h X. U. h ) ) )
92	91	rexlimiv	|- ( E. t e. h u = ( { t } X. t ) -> u e. ~P ( h X. U. h ) )
93	92	adantl	|- ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) -> u e. ~P ( h X. U. h ) )
94	93	abssi	|- { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } C_ ~P ( h X. U. h )
95	81 94	ssexi	|- { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } e. _V
96	1 95	eqeltri	|- A e. _V
97		raleq	|- ( x = A -> ( A. z e. x z =/= (/) <-> A. z e. A z =/= (/) ) )
98		raleq	|- ( x = A -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) )
99	98	raleqbi1dv	|- ( 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 ) = (/) ) ) )
100	97 99	anbi12d	|- ( 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 ) = (/) ) ) ) )
101		raleq	|- ( 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 ) ) )
102	101	exbidv	|- ( 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 ) ) )
103	100 102	imbi12d	|- ( 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 ) ) ) )
104	96 103	spcv	|- ( 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 ) ) )
105	3 104	sylbi	|- ( 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 ) ) )
106	12 77 105	mp2ani	|- ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )