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 ) )