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