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