Metamath Proof Explorer

Theorem cantnf2

Description: For every ordinal, A , there is a an ordinal exponent b such that A is less than ( _om ^o b ) and for every ordinal at least as large as b there is a unique Cantor normal form, f , with zeros for all the unnecessary higher terms, that sums to A . Theorem 5.3 of Schloeder p. 16. (Contributed by RP, 3-Feb-2025)

Ref Expression
Assertion cantnf2 
|- ( A e. On -> E. b e. On A. c e. ( On \ b ) E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) )

Proof

Step Hyp Ref Expression
1 onexoegt 
 |-  ( A e. On -> E. b e. On A e. ( _om ^o b ) )
2 eldif 
 |-  ( c e. ( On \ b ) <-> ( c e. On /\ -. c e. b ) )
3 simp2 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> b e. On )
4 pm3.2 
 |-  ( b e. On -> ( c e. On -> ( b e. On /\ c e. On ) ) )
5 3 4 syl 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> ( c e. On -> ( b e. On /\ c e. On ) ) )
6 ontri1 
 |-  ( ( b e. On /\ c e. On ) -> ( b C_ c <-> -. c e. b ) )
7 5 6 syl6 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> ( c e. On -> ( b C_ c <-> -. c e. b ) ) )
8 7 pm5.32d 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> ( ( c e. On /\ b C_ c ) <-> ( c e. On /\ -. c e. b ) ) )
9 2 8 bitr4id 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> ( c e. ( On \ b ) <-> ( c e. On /\ b C_ c ) ) )
10 simplr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> a = A )
11 10 breq2d 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> ( f ( _om CNF c ) a <-> f ( _om CNF c ) A ) )
12 eqid 
 |-  dom ( _om CNF c ) = dom ( _om CNF c )
13 omelon 
 |-  _om e. On
14 13 a1i 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> _om e. On )
15 simprl 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> c e. On )
16 15 ad2antrr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> c e. On )
17 12 14 16 cantnff1o 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> ( _om CNF c ) : dom ( _om CNF c ) -1-1-onto-> ( _om ^o c ) )
18 f1ofun 
 |-  ( ( _om CNF c ) : dom ( _om CNF c ) -1-1-onto-> ( _om ^o c ) -> Fun ( _om CNF c ) )
19 17 18 syl 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> Fun ( _om CNF c ) )
20 funbrfvb 
 |-  ( ( Fun ( _om CNF c ) /\ f e. dom ( _om CNF c ) ) -> ( ( ( _om CNF c ) ` f ) = A <-> f ( _om CNF c ) A ) )
21 19 20 sylancom 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> ( ( ( _om CNF c ) ` f ) = A <-> f ( _om CNF c ) A ) )
22 11 21 bitr4d 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) /\ f e. dom ( _om CNF c ) ) -> ( f ( _om CNF c ) a <-> ( ( _om CNF c ) ` f ) = A ) )
23 22 reubidva 
 |-  ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ a = A ) -> ( E! f e. dom ( _om CNF c ) f ( _om CNF c ) a <-> E! f e. dom ( _om CNF c ) ( ( _om CNF c ) ` f ) = A ) )
24 simpl2 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> b e. On )
25 13 a1i 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> _om e. On )
26 24 15 25 3jca 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> ( b e. On /\ c e. On /\ _om e. On ) )
27 peano1 
 |-  (/) e. _om
28 26 27 jctir 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> ( ( b e. On /\ c e. On /\ _om e. On ) /\ (/) e. _om ) )
29 simprr 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> b C_ c )
30 oewordi 
 |-  ( ( ( b e. On /\ c e. On /\ _om e. On ) /\ (/) e. _om ) -> ( b C_ c -> ( _om ^o b ) C_ ( _om ^o c ) ) )
31 28 29 30 sylc 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> ( _om ^o b ) C_ ( _om ^o c ) )
32 simpl3 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> A e. ( _om ^o b ) )
33 31 32 sseldd 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> A e. ( _om ^o c ) )
34 12 25 15 cantnff1o 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> ( _om CNF c ) : dom ( _om CNF c ) -1-1-onto-> ( _om ^o c ) )
35 dff1o5 
 |-  ( ( _om CNF c ) : dom ( _om CNF c ) -1-1-onto-> ( _om ^o c ) <-> ( ( _om CNF c ) : dom ( _om CNF c ) -1-1-> ( _om ^o c ) /\ ran ( _om CNF c ) = ( _om ^o c ) ) )
36 simpr 
 |-  ( ( ( _om CNF c ) : dom ( _om CNF c ) -1-1-> ( _om ^o c ) /\ ran ( _om CNF c ) = ( _om ^o c ) ) -> ran ( _om CNF c ) = ( _om ^o c ) )
37 35 36 sylbi 
 |-  ( ( _om CNF c ) : dom ( _om CNF c ) -1-1-onto-> ( _om ^o c ) -> ran ( _om CNF c ) = ( _om ^o c ) )
38 34 37 syl 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> ran ( _om CNF c ) = ( _om ^o c ) )
39 33 38 eleqtrrd 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> A e. ran ( _om CNF c ) )
40 dff1o2 
 |-  ( ( _om CNF c ) : dom ( _om CNF c ) -1-1-onto-> ( _om ^o c ) <-> ( ( _om CNF c ) Fn dom ( _om CNF c ) /\ Fun `' ( _om CNF c ) /\ ran ( _om CNF c ) = ( _om ^o c ) ) )
41 simp2 
 |-  ( ( ( _om CNF c ) Fn dom ( _om CNF c ) /\ Fun `' ( _om CNF c ) /\ ran ( _om CNF c ) = ( _om ^o c ) ) -> Fun `' ( _om CNF c ) )
42 40 41 sylbi 
 |-  ( ( _om CNF c ) : dom ( _om CNF c ) -1-1-onto-> ( _om ^o c ) -> Fun `' ( _om CNF c ) )
43 34 42 syl 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> Fun `' ( _om CNF c ) )
44 funcnv3 
 |-  ( Fun `' ( _om CNF c ) <-> A. a e. ran ( _om CNF c ) E! f e. dom ( _om CNF c ) f ( _om CNF c ) a )
45 43 44 sylib 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> A. a e. ran ( _om CNF c ) E! f e. dom ( _om CNF c ) f ( _om CNF c ) a )
46 23 39 45 rspcdv2 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> E! f e. dom ( _om CNF c ) ( ( _om CNF c ) ` f ) = A )
47 32 ad2antrr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> A e. ( _om ^o b ) )
48 simplr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> f e. dom ( _om CNF c ) )
49 13 a1i 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> _om e. On )
50 15 ad2antrr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> c e. On )
51 12 49 50 cantnfs 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( f e. dom ( _om CNF c ) <-> ( f : c --> _om /\ f finSupp (/) ) ) )
52 48 51 mpbid 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( f : c --> _om /\ f finSupp (/) ) )
53 simpr 
 |-  ( ( f : c --> _om /\ f finSupp (/) ) -> f finSupp (/) )
54 52 53 syl 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> f finSupp (/) )
55 eqid 
 |-  dom ( _om CNF b ) = dom ( _om CNF b )
56 24 ad2antrr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> b e. On )
57 29 ad2antrr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> b C_ c )
58 simpr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( _om CNF c ) ` f ) = A )
59 58 47 eqeltrd 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( _om CNF c ) ` f ) e. ( _om ^o b ) )
60 1onn 
 |-  1o e. _om
61 ondif2 
 |-  ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) )
62 13 60 61 mpbir2an 
 |-  _om e. ( On \ 2o )
63 62 a1i 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> _om e. ( On \ 2o ) )
64 cantnfresb 
 |-  ( ( ( _om e. ( On \ 2o ) /\ c e. On ) /\ ( b e. On /\ f e. dom ( _om CNF c ) ) ) -> ( ( ( _om CNF c ) ` f ) e. ( _om ^o b ) <-> A. d e. ( c \ b ) ( f ` d ) = (/) ) )
65 63 50 56 48 64 syl22anc 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( ( _om CNF c ) ` f ) e. ( _om ^o b ) <-> A. d e. ( c \ b ) ( f ` d ) = (/) ) )
66 59 65 mpbid 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> A. d e. ( c \ b ) ( f ` d ) = (/) )
67 66 r19.21bi 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. ( c \ b ) ) -> ( f ` d ) = (/) )
68 27 a1i 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> (/) e. _om )
69 simpllr 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> f e. dom ( _om CNF c ) )
70 13 a1i 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> _om e. On )
71 15 adantr 
 |-  ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) -> c e. On )
72 71 ad2antrr 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> c e. On )
73 12 70 72 cantnfs 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> ( f e. dom ( _om CNF c ) <-> ( f : c --> _om /\ f finSupp (/) ) ) )
74 69 73 mpbid 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> ( f : c --> _om /\ f finSupp (/) ) )
75 74 simpld 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> f : c --> _om )
76 57 sselda 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> d e. c )
77 75 76 ffvelcdmd 
 |-  ( ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) /\ d e. b ) -> ( f ` d ) e. _om )
78 77 fmpttd 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( d e. b |-> ( f ` d ) ) : b --> _om )
79 12 25 15 cantnfs 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> ( f e. dom ( _om CNF c ) <-> ( f : c --> _om /\ f finSupp (/) ) ) )
80 79 simprbda 
 |-  ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) -> f : c --> _om )
81 80 adantr 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> f : c --> _om )
82 81 57 feqresmpt 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( f |` b ) = ( d e. b |-> ( f ` d ) ) )
83 54 68 fsuppres 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( f |` b ) finSupp (/) )
84 82 83 eqbrtrrd 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( d e. b |-> ( f ` d ) ) finSupp (/) )
85 55 49 56 cantnfs 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( d e. b |-> ( f ` d ) ) e. dom ( _om CNF b ) <-> ( ( d e. b |-> ( f ` d ) ) : b --> _om /\ ( d e. b |-> ( f ` d ) ) finSupp (/) ) ) )
86 78 84 85 mpbir2and 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( d e. b |-> ( f ` d ) ) e. dom ( _om CNF b ) )
87 55 49 56 50 57 67 68 12 86 cantnfres 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( _om CNF b ) ` ( d e. b |-> ( f ` d ) ) ) = ( ( _om CNF c ) ` ( d e. c |-> ( f ` d ) ) ) )
88 82 fveq2d 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( _om CNF b ) ` ( f |` b ) ) = ( ( _om CNF b ) ` ( d e. b |-> ( f ` d ) ) ) )
89 81 feqmptd 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> f = ( d e. c |-> ( f ` d ) ) )
90 89 fveq2d 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( _om CNF c ) ` f ) = ( ( _om CNF c ) ` ( d e. c |-> ( f ` d ) ) ) )
91 87 88 90 3eqtr4d 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( _om CNF b ) ` ( f |` b ) ) = ( ( _om CNF c ) ` f ) )
92 91 58 eqtrd 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( ( _om CNF b ) ` ( f |` b ) ) = A )
93 47 54 92 3jca 
 |-  ( ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) /\ ( ( _om CNF c ) ` f ) = A ) -> ( A e. ( _om ^o b ) /\ f finSupp (/) /\ ( ( _om CNF b ) ` ( f |` b ) ) = A ) )
94 93 ex 
 |-  ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) -> ( ( ( _om CNF c ) ` f ) = A -> ( A e. ( _om ^o b ) /\ f finSupp (/) /\ ( ( _om CNF b ) ` ( f |` b ) ) = A ) ) )
95 94 pm4.71rd 
 |-  ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) -> ( ( ( _om CNF c ) ` f ) = A <-> ( ( A e. ( _om ^o b ) /\ f finSupp (/) /\ ( ( _om CNF b ) ` ( f |` b ) ) = A ) /\ ( ( _om CNF c ) ` f ) = A ) ) )
96 3an4anass 
 |-  ( ( ( A e. ( _om ^o b ) /\ f finSupp (/) /\ ( ( _om CNF b ) ` ( f |` b ) ) = A ) /\ ( ( _om CNF c ) ` f ) = A ) <-> ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) )
97 95 96 bitrdi 
 |-  ( ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) /\ f e. dom ( _om CNF c ) ) -> ( ( ( _om CNF c ) ` f ) = A <-> ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) ) )
98 97 reubidva 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> ( E! f e. dom ( _om CNF c ) ( ( _om CNF c ) ` f ) = A <-> E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) ) )
99 46 98 mpbid 
 |-  ( ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) /\ ( c e. On /\ b C_ c ) ) -> E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) )
100 99 ex 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> ( ( c e. On /\ b C_ c ) -> E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) ) )
101 9 100 sylbid 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> ( c e. ( On \ b ) -> E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) ) )
102 101 ralrimiv 
 |-  ( ( A e. On /\ b e. On /\ A e. ( _om ^o b ) ) -> A. c e. ( On \ b ) E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) )
103 102 3exp 
 |-  ( A e. On -> ( b e. On -> ( A e. ( _om ^o b ) -> A. c e. ( On \ b ) E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) ) ) )
104 103 reximdvai 
 |-  ( A e. On -> ( E. b e. On A e. ( _om ^o b ) -> E. b e. On A. c e. ( On \ b ) E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) ) )
105 1 104 mpd 
 |-  ( A e. On -> E. b e. On A. c e. ( On \ b ) E! f e. dom ( _om CNF c ) ( ( A e. ( _om ^o b ) /\ f finSupp (/) ) /\ ( ( ( _om CNF b ) ` ( f |` b ) ) = A /\ ( ( _om CNF c ) ` f ) = A ) ) )