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