Metamath Proof Explorer


Theorem cantnflt2

Description: An upper bound on the CNF function. (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 29-Jun-2019)

Ref Expression
Hypotheses cantnfs.s
|- S = dom ( A CNF B )
cantnfs.a
|- ( ph -> A e. On )
cantnfs.b
|- ( ph -> B e. On )
cantnflt2.f
|- ( ph -> F e. S )
cantnflt2.a
|- ( ph -> (/) e. A )
cantnflt2.c
|- ( ph -> C e. On )
cantnflt2.s
|- ( ph -> ( F supp (/) ) C_ C )
Assertion cantnflt2
|- ( ph -> ( ( A CNF B ) ` F ) e. ( A ^o C ) )

Proof

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