This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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