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 |
|
cantnflt2.f |
|- ( ph -> F e. S ) |
5 |
|
cantnflt2.a |
|- ( ph -> (/) e. A ) |
6 |
|
cantnflt2.c |
|- ( ph -> C e. On ) |
7 |
|
cantnflt2.s |
|- ( ph -> ( F supp (/) ) C_ C ) |
8 |
|
eqid |
|- OrdIso ( _E , ( F supp (/) ) ) = OrdIso ( _E , ( F supp (/) ) ) |
9 |
|
eqid |
|- seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) .o ( F ` ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) .o ( F ` ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) |
10 |
1 2 3 8 4 9
|
cantnfval |
|- ( ph -> ( ( A CNF B ) ` F ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) .o ( F ` ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( F supp (/) ) ) ) ) |
11 |
|
ovexd |
|- ( ph -> ( F supp (/) ) e. _V ) |
12 |
8
|
oion |
|- ( ( F supp (/) ) e. _V -> dom OrdIso ( _E , ( F supp (/) ) ) e. On ) |
13 |
|
sucidg |
|- ( dom OrdIso ( _E , ( F supp (/) ) ) e. On -> dom OrdIso ( _E , ( F supp (/) ) ) e. suc dom OrdIso ( _E , ( F supp (/) ) ) ) |
14 |
11 12 13
|
3syl |
|- ( ph -> dom OrdIso ( _E , ( F supp (/) ) ) e. suc dom OrdIso ( _E , ( F supp (/) ) ) ) |
15 |
1 2 3 8 4
|
cantnfcl |
|- ( ph -> ( _E We ( F supp (/) ) /\ dom OrdIso ( _E , ( F supp (/) ) ) e. _om ) ) |
16 |
15
|
simpld |
|- ( ph -> _E We ( F supp (/) ) ) |
17 |
8
|
oiiso |
|- ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> OrdIso ( _E , ( F supp (/) ) ) Isom _E , _E ( dom OrdIso ( _E , ( F supp (/) ) ) , ( F supp (/) ) ) ) |
18 |
11 16 17
|
syl2anc |
|- ( ph -> OrdIso ( _E , ( F supp (/) ) ) Isom _E , _E ( dom OrdIso ( _E , ( F supp (/) ) ) , ( F supp (/) ) ) ) |
19 |
|
isof1o |
|- ( OrdIso ( _E , ( F supp (/) ) ) Isom _E , _E ( dom OrdIso ( _E , ( F supp (/) ) ) , ( F supp (/) ) ) -> OrdIso ( _E , ( F supp (/) ) ) : dom OrdIso ( _E , ( F supp (/) ) ) -1-1-onto-> ( F supp (/) ) ) |
20 |
|
f1ofo |
|- ( OrdIso ( _E , ( F supp (/) ) ) : dom OrdIso ( _E , ( F supp (/) ) ) -1-1-onto-> ( F supp (/) ) -> OrdIso ( _E , ( F supp (/) ) ) : dom OrdIso ( _E , ( F supp (/) ) ) -onto-> ( F supp (/) ) ) |
21 |
|
foima |
|- ( OrdIso ( _E , ( F supp (/) ) ) : dom OrdIso ( _E , ( F supp (/) ) ) -onto-> ( F supp (/) ) -> ( OrdIso ( _E , ( F supp (/) ) ) " dom OrdIso ( _E , ( F supp (/) ) ) ) = ( F supp (/) ) ) |
22 |
18 19 20 21
|
4syl |
|- ( ph -> ( OrdIso ( _E , ( F supp (/) ) ) " dom OrdIso ( _E , ( F supp (/) ) ) ) = ( F supp (/) ) ) |
23 |
22 7
|
eqsstrd |
|- ( ph -> ( OrdIso ( _E , ( F supp (/) ) ) " dom OrdIso ( _E , ( F supp (/) ) ) ) C_ C ) |
24 |
1 2 3 8 4 9 5 14 6 23
|
cantnflt |
|- ( ph -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) .o ( F ` ( OrdIso ( _E , ( F supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( F supp (/) ) ) ) e. ( A ^o C ) ) |
25 |
10 24
|
eqeltrd |
|- ( ph -> ( ( A CNF B ) ` F ) e. ( A ^o C ) ) |