Metamath Proof Explorer

Theorem cantnf0

Description: The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnf0.a 
|- ( ph -> (/) e. A )
Assertion cantnf0 
|- ( ph -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (/) )

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 cantnf0.a 
 |-  ( ph -> (/) e. A )
5 eqid 
 |-  OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) = OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) )
6 fconst6g 
 |-  ( (/) e. A -> ( B X. { (/) } ) : B --> A )
7 4 6 syl 
 |-  ( ph -> ( B X. { (/) } ) : B --> A )
8 3 4 fczfsuppd 
 |-  ( ph -> ( B X. { (/) } ) finSupp (/) )
9 1 2 3 cantnfs 
 |-  ( ph -> ( ( B X. { (/) } ) e. S <-> ( ( B X. { (/) } ) : B --> A /\ ( B X. { (/) } ) finSupp (/) ) ) )
10 7 8 9 mpbir2and 
 |-  ( ph -> ( B X. { (/) } ) e. S )
11 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
12 1 2 3 5 10 11 cantnfval 
 |-  ( ph -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ) )
13 eqidd 
 |-  ( ph -> ( B X. { (/) } ) = ( B X. { (/) } ) )
14 0ex 
 |-  (/) e. _V
15 fnconstg 
 |-  ( (/) e. _V -> ( B X. { (/) } ) Fn B )
16 14 15 mp1i 
 |-  ( ph -> ( B X. { (/) } ) Fn B )
17 14 a1i 
 |-  ( ph -> (/) e. _V )
18 fnsuppeq0 
 |-  ( ( ( B X. { (/) } ) Fn B /\ B e. On /\ (/) e. _V ) -> ( ( ( B X. { (/) } ) supp (/) ) = (/) <-> ( B X. { (/) } ) = ( B X. { (/) } ) ) )
19 16 3 17 18 syl3anc 
 |-  ( ph -> ( ( ( B X. { (/) } ) supp (/) ) = (/) <-> ( B X. { (/) } ) = ( B X. { (/) } ) ) )
20 13 19 mpbird 
 |-  ( ph -> ( ( B X. { (/) } ) supp (/) ) = (/) )
21 oieq2 
 |-  ( ( ( B X. { (/) } ) supp (/) ) = (/) -> OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) = OrdIso ( _E , (/) ) )
22 20 21 syl 
 |-  ( ph -> OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) = OrdIso ( _E , (/) ) )
23 22 dmeqd 
 |-  ( ph -> dom OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) = dom OrdIso ( _E , (/) ) )
24 we0 
 |-  _E We (/)
25 eqid 
 |-  OrdIso ( _E , (/) ) = OrdIso ( _E , (/) )
26 25 oien 
 |-  ( ( (/) e. _V /\ _E We (/) ) -> dom OrdIso ( _E , (/) ) ~~ (/) )
27 14 24 26 mp2an 
 |-  dom OrdIso ( _E , (/) ) ~~ (/)
28 en0 
 |-  ( dom OrdIso ( _E , (/) ) ~~ (/) <-> dom OrdIso ( _E , (/) ) = (/) )
29 27 28 mpbi 
 |-  dom OrdIso ( _E , (/) ) = (/)
30 23 29 eqtrdi 
 |-  ( ph -> dom OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) = (/) )
31 30 fveq2d 
 |-  ( ph -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) )
32 11 seqom0g 
 |-  ( (/) e. _V -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
33 14 32 mp1i 
 |-  ( ph -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
34 12 31 33 3eqtrd 
 |-  ( ph -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (/) )