Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
|- S = dom ( A CNF B ) |
2 |
|
cantnfs.a |
|- ( ph -> A e. On ) |
3 |
|
cantnfs.b |
|- ( ph -> B e. On ) |
4 |
|
oemapval.t |
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } |
5 |
|
eloni |
|- ( B e. On -> Ord B ) |
6 |
|
ordwe |
|- ( Ord B -> _E We B ) |
7 |
|
weso |
|- ( _E We B -> _E Or B ) |
8 |
3 5 6 7
|
4syl |
|- ( ph -> _E Or B ) |
9 |
|
cnvso |
|- ( _E Or B <-> `' _E Or B ) |
10 |
8 9
|
sylib |
|- ( ph -> `' _E Or B ) |
11 |
|
eloni |
|- ( A e. On -> Ord A ) |
12 |
|
ordwe |
|- ( Ord A -> _E We A ) |
13 |
|
weso |
|- ( _E We A -> _E Or A ) |
14 |
2 11 12 13
|
4syl |
|- ( ph -> _E Or A ) |
15 |
|
fvex |
|- ( y ` z ) e. _V |
16 |
15
|
epeli |
|- ( ( x ` z ) _E ( y ` z ) <-> ( x ` z ) e. ( y ` z ) ) |
17 |
|
vex |
|- w e. _V |
18 |
|
vex |
|- z e. _V |
19 |
17 18
|
brcnv |
|- ( w `' _E z <-> z _E w ) |
20 |
|
epel |
|- ( z _E w <-> z e. w ) |
21 |
19 20
|
bitri |
|- ( w `' _E z <-> z e. w ) |
22 |
21
|
imbi1i |
|- ( ( w `' _E z -> ( x ` w ) = ( y ` w ) ) <-> ( z e. w -> ( x ` w ) = ( y ` w ) ) ) |
23 |
22
|
ralbii |
|- ( A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) |
24 |
16 23
|
anbi12i |
|- ( ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) ) |
25 |
24
|
rexbii |
|- ( E. z e. B ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) ) |
26 |
25
|
opabbii |
|- { <. x , y >. | E. z e. B ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) } = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } |
27 |
4 26
|
eqtr4i |
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) } |
28 |
|
breq1 |
|- ( g = x -> ( g finSupp (/) <-> x finSupp (/) ) ) |
29 |
28
|
cbvrabv |
|- { g e. ( A ^m B ) | g finSupp (/) } = { x e. ( A ^m B ) | x finSupp (/) } |
30 |
27 29
|
wemapso2 |
|- ( ( B e. On /\ `' _E Or B /\ _E Or A ) -> T Or { g e. ( A ^m B ) | g finSupp (/) } ) |
31 |
3 10 14 30
|
syl3anc |
|- ( ph -> T Or { g e. ( A ^m B ) | g finSupp (/) } ) |
32 |
|
eqid |
|- { g e. ( A ^m B ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) } |
33 |
32 2 3
|
cantnfdm |
|- ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } ) |
34 |
1 33
|
eqtrid |
|- ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } ) |
35 |
|
soeq2 |
|- ( S = { g e. ( A ^m B ) | g finSupp (/) } -> ( T Or S <-> T Or { g e. ( A ^m B ) | g finSupp (/) } ) ) |
36 |
34 35
|
syl |
|- ( ph -> ( T Or S <-> T Or { g e. ( A ^m B ) | g finSupp (/) } ) ) |
37 |
31 36
|
mpbird |
|- ( ph -> T Or S ) |