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 |
|
oecl |
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On ) |
6 |
2 3 5
|
syl2anc |
|- ( ph -> ( A ^o B ) e. On ) |
7 |
|
eloni |
|- ( ( A ^o B ) e. On -> Ord ( A ^o B ) ) |
8 |
|
ordwe |
|- ( Ord ( A ^o B ) -> _E We ( A ^o B ) ) |
9 |
6 7 8
|
3syl |
|- ( ph -> _E We ( A ^o B ) ) |
10 |
1 2 3 4
|
cantnf |
|- ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) ) |
11 |
|
isowe |
|- ( ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) -> ( T We S <-> _E We ( A ^o B ) ) ) |
12 |
10 11
|
syl |
|- ( ph -> ( T We S <-> _E We ( A ^o B ) ) ) |
13 |
9 12
|
mpbird |
|- ( ph -> T We S ) |
14 |
6 7
|
syl |
|- ( ph -> Ord ( A ^o B ) ) |
15 |
|
isocnv |
|- ( ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) -> `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) |
16 |
10 15
|
syl |
|- ( ph -> `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) |
17 |
|
ovex |
|- ( A CNF B ) e. _V |
18 |
17
|
dmex |
|- dom ( A CNF B ) e. _V |
19 |
1 18
|
eqeltri |
|- S e. _V |
20 |
|
exse |
|- ( S e. _V -> T Se S ) |
21 |
19 20
|
ax-mp |
|- T Se S |
22 |
|
eqid |
|- OrdIso ( T , S ) = OrdIso ( T , S ) |
23 |
22
|
oieu |
|- ( ( T We S /\ T Se S ) -> ( ( Ord ( A ^o B ) /\ `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) <-> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) ) ) |
24 |
13 21 23
|
sylancl |
|- ( ph -> ( ( Ord ( A ^o B ) /\ `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) <-> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) ) ) |
25 |
14 16 24
|
mpbi2and |
|- ( ph -> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) ) |
26 |
25
|
simpld |
|- ( ph -> ( A ^o B ) = dom OrdIso ( T , S ) ) |
27 |
26
|
eqcomd |
|- ( ph -> dom OrdIso ( T , S ) = ( A ^o B ) ) |
28 |
13 27
|
jca |
|- ( ph -> ( T We S /\ dom OrdIso ( T , S ) = ( A ^o B ) ) ) |