Metamath Proof Explorer

Theorem dfac5lem3

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 dfac5lem3 
|- ( ( { w } X. w ) e. A <-> ( w =/= (/) /\ w e. h ) )

Proof

Step Hyp Ref Expression
1 dfac5lem.1 
 |-  A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
2 vsnex 
 |-  { w } e. _V
3 vex 
 |-  w e. _V
4 2 3 xpex 
 |-  ( { w } X. w ) e. _V
5 neeq1 
 |-  ( u = ( { w } X. w ) -> ( u =/= (/) <-> ( { w } X. w ) =/= (/) ) )
6 eqeq1 
 |-  ( u = ( { w } X. w ) -> ( u = ( { t } X. t ) <-> ( { w } X. w ) = ( { t } X. t ) ) )
7 6 rexbidv 
 |-  ( u = ( { w } X. w ) -> ( E. t e. h u = ( { t } X. t ) <-> E. t e. h ( { w } X. w ) = ( { t } X. t ) ) )
8 5 7 anbi12d 
 |-  ( u = ( { w } X. w ) -> ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) <-> ( ( { w } X. w ) =/= (/) /\ E. t e. h ( { w } X. w ) = ( { t } X. t ) ) ) )
9 4 8 elab 
 |-  ( ( { w } X. w ) e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } <-> ( ( { w } X. w ) =/= (/) /\ E. t e. h ( { w } X. w ) = ( { t } X. t ) ) )
10 1 eleq2i 
 |-  ( ( { w } X. w ) e. A <-> ( { w } X. w ) e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } )
11 xpeq2 
 |-  ( w = (/) -> ( { w } X. w ) = ( { w } X. (/) ) )
12 xp0 
 |-  ( { w } X. (/) ) = (/)
13 11 12 eqtrdi 
 |-  ( w = (/) -> ( { w } X. w ) = (/) )
14 rneq 
 |-  ( ( { w } X. w ) = (/) -> ran ( { w } X. w ) = ran (/) )
15 3 snnz 
 |-  { w } =/= (/)
16 rnxp 
 |-  ( { w } =/= (/) -> ran ( { w } X. w ) = w )
17 15 16 ax-mp 
 |-  ran ( { w } X. w ) = w
18 rn0 
 |-  ran (/) = (/)
19 14 17 18 3eqtr3g 
 |-  ( ( { w } X. w ) = (/) -> w = (/) )
20 13 19 impbii 
 |-  ( w = (/) <-> ( { w } X. w ) = (/) )
21 20 necon3bii 
 |-  ( w =/= (/) <-> ( { w } X. w ) =/= (/) )
22 df-rex 
 |-  ( E. t e. h ( { w } X. w ) = ( { t } X. t ) <-> E. t ( t e. h /\ ( { w } X. w ) = ( { t } X. t ) ) )
23 rneq 
 |-  ( ( { w } X. w ) = ( { t } X. t ) -> ran ( { w } X. w ) = ran ( { t } X. t ) )
24 vex 
 |-  t e. _V
25 24 snnz 
 |-  { t } =/= (/)
26 rnxp 
 |-  ( { t } =/= (/) -> ran ( { t } X. t ) = t )
27 25 26 ax-mp 
 |-  ran ( { t } X. t ) = t
28 23 17 27 3eqtr3g 
 |-  ( ( { w } X. w ) = ( { t } X. t ) -> w = t )
29 sneq 
 |-  ( w = t -> { w } = { t } )
30 29 xpeq1d 
 |-  ( w = t -> ( { w } X. w ) = ( { t } X. w ) )
31 xpeq2 
 |-  ( w = t -> ( { t } X. w ) = ( { t } X. t ) )
32 30 31 eqtrd 
 |-  ( w = t -> ( { w } X. w ) = ( { t } X. t ) )
33 28 32 impbii 
 |-  ( ( { w } X. w ) = ( { t } X. t ) <-> w = t )
34 equcom 
 |-  ( w = t <-> t = w )
35 33 34 bitri 
 |-  ( ( { w } X. w ) = ( { t } X. t ) <-> t = w )
36 35 anbi1ci 
 |-  ( ( t e. h /\ ( { w } X. w ) = ( { t } X. t ) ) <-> ( t = w /\ t e. h ) )
37 36 exbii 
 |-  ( E. t ( t e. h /\ ( { w } X. w ) = ( { t } X. t ) ) <-> E. t ( t = w /\ t e. h ) )
38 elequ1 
 |-  ( t = w -> ( t e. h <-> w e. h ) )
39 38 equsexvw 
 |-  ( E. t ( t = w /\ t e. h ) <-> w e. h )
40 22 37 39 3bitrri 
 |-  ( w e. h <-> E. t e. h ( { w } X. w ) = ( { t } X. t ) )
41 21 40 anbi12i 
 |-  ( ( w =/= (/) /\ w e. h ) <-> ( ( { w } X. w ) =/= (/) /\ E. t e. h ( { w } X. w ) = ( { t } X. t ) ) )
42 9 10 41 3bitr4i 
 |-  ( ( { w } X. w ) e. A <-> ( w =/= (/) /\ w e. h ) )