Metamath Proof Explorer

Theorem dfac5lem2

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

Ref Expression
Hypothesis dfac5lem.1 
|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
Assertion dfac5lem2 
|- ( <. w , g >. e. U. A <-> ( w e. h /\ g e. w ) )

Proof

Step Hyp Ref Expression
1 dfac5lem.1 
 |-  A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
2 1 unieqi 
 |-  U. A = U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
3 2 eleq2i 
 |-  ( <. w , g >. e. U. A <-> <. w , g >. e. U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } )
4 eluniab 
 |-  ( <. w , g >. e. U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } <-> E. u ( <. w , g >. e. u /\ ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) ) )
5 r19.42v 
 |-  ( E. t e. h ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> ( ( <. w , g >. e. u /\ u =/= (/) ) /\ E. t e. h u = ( { t } X. t ) ) )
6 anass 
 |-  ( ( ( <. w , g >. e. u /\ u =/= (/) ) /\ E. t e. h u = ( { t } X. t ) ) <-> ( <. w , g >. e. u /\ ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) ) )
7 5 6 bitr2i 
 |-  ( ( <. w , g >. e. u /\ ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) ) <-> E. t e. h ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) )
8 7 exbii 
 |-  ( E. u ( <. w , g >. e. u /\ ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) ) <-> E. u E. t e. h ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) )
9 rexcom4 
 |-  ( E. t e. h E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> E. u E. t e. h ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) )
10 df-rex 
 |-  ( E. t e. h E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> E. t ( t e. h /\ E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) ) )
11 9 10 bitr3i 
 |-  ( E. u E. t e. h ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> E. t ( t e. h /\ E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) ) )
12 4 8 11 3bitri 
 |-  ( <. w , g >. e. U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } <-> E. t ( t e. h /\ E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) ) )
13 ancom 
 |-  ( ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> ( u = ( { t } X. t ) /\ ( <. w , g >. e. u /\ u =/= (/) ) ) )
14 ne0i 
 |-  ( <. w , g >. e. u -> u =/= (/) )
15 14 pm4.71i 
 |-  ( <. w , g >. e. u <-> ( <. w , g >. e. u /\ u =/= (/) ) )
16 15 anbi2i 
 |-  ( ( u = ( { t } X. t ) /\ <. w , g >. e. u ) <-> ( u = ( { t } X. t ) /\ ( <. w , g >. e. u /\ u =/= (/) ) ) )
17 13 16 bitr4i 
 |-  ( ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> ( u = ( { t } X. t ) /\ <. w , g >. e. u ) )
18 17 exbii 
 |-  ( E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> E. u ( u = ( { t } X. t ) /\ <. w , g >. e. u ) )
19 snex 
 |-  { t } e. _V
20 vex 
 |-  t e. _V
21 19 20 xpex 
 |-  ( { t } X. t ) e. _V
22 eleq2 
 |-  ( u = ( { t } X. t ) -> ( <. w , g >. e. u <-> <. w , g >. e. ( { t } X. t ) ) )
23 21 22 ceqsexv 
 |-  ( E. u ( u = ( { t } X. t ) /\ <. w , g >. e. u ) <-> <. w , g >. e. ( { t } X. t ) )
24 18 23 bitri 
 |-  ( E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) <-> <. w , g >. e. ( { t } X. t ) )
25 24 anbi2i 
 |-  ( ( t e. h /\ E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) ) <-> ( t e. h /\ <. w , g >. e. ( { t } X. t ) ) )
26 opelxp 
 |-  ( <. w , g >. e. ( { t } X. t ) <-> ( w e. { t } /\ g e. t ) )
27 velsn 
 |-  ( w e. { t } <-> w = t )
28 equcom 
 |-  ( w = t <-> t = w )
29 27 28 bitri 
 |-  ( w e. { t } <-> t = w )
30 29 anbi1i 
 |-  ( ( w e. { t } /\ g e. t ) <-> ( t = w /\ g e. t ) )
31 26 30 bitri 
 |-  ( <. w , g >. e. ( { t } X. t ) <-> ( t = w /\ g e. t ) )
32 31 anbi2i 
 |-  ( ( t e. h /\ <. w , g >. e. ( { t } X. t ) ) <-> ( t e. h /\ ( t = w /\ g e. t ) ) )
33 an12 
 |-  ( ( t e. h /\ ( t = w /\ g e. t ) ) <-> ( t = w /\ ( t e. h /\ g e. t ) ) )
34 25 32 33 3bitri 
 |-  ( ( t e. h /\ E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) ) <-> ( t = w /\ ( t e. h /\ g e. t ) ) )
35 34 exbii 
 |-  ( E. t ( t e. h /\ E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) ) <-> E. t ( t = w /\ ( t e. h /\ g e. t ) ) )
36 vex 
 |-  w e. _V
37 elequ1 
 |-  ( t = w -> ( t e. h <-> w e. h ) )
38 eleq2 
 |-  ( t = w -> ( g e. t <-> g e. w ) )
39 37 38 anbi12d 
 |-  ( t = w -> ( ( t e. h /\ g e. t ) <-> ( w e. h /\ g e. w ) ) )
40 36 39 ceqsexv 
 |-  ( E. t ( t = w /\ ( t e. h /\ g e. t ) ) <-> ( w e. h /\ g e. w ) )
41 35 40 bitri 
 |-  ( E. t ( t e. h /\ E. u ( ( <. w , g >. e. u /\ u =/= (/) ) /\ u = ( { t } X. t ) ) ) <-> ( w e. h /\ g e. w ) )
42 3 12 41 3bitri 
 |-  ( <. w , g >. e. U. A <-> ( w e. h /\ g e. w ) )