Metamath Proof Explorer

Theorem cantnflem3

Description: Lemma for cantnf . Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than C has a normal form, we can use oeeu to factor C into the form ( ( A ^o X ) .o Y ) +o Z where 0 < Y < A and Z < ( A ^o X ) (and a fortiori X < B ). Then since Z < ( A ^o X ) <_ ( A ^o X ) .o Y <_ C , Z has a normal form, and by appending the term ( A ^o X ) .o Y using cantnfp1 we get a normal form for C . (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
oemapval.t 
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
cantnf.c 
|- ( ph -> C e. ( A ^o B ) )
cantnf.s 
|- ( ph -> C C_ ran ( A CNF B ) )
cantnf.e 
|- ( ph -> (/) e. C )
cantnf.x 
|- X = U. |^| { c e. On | C e. ( A ^o c ) }
cantnf.p 
|- P = ( iota d E. a e. On E. b e. ( A ^o X ) ( d = <. a , b >. /\ ( ( ( A ^o X ) .o a ) +o b ) = C ) )
cantnf.y 
|- Y = ( 1st ` P )
cantnf.z 
|- Z = ( 2nd ` P )
cantnf.g 
|- ( ph -> G e. S )
cantnf.v 
|- ( ph -> ( ( A CNF B ) ` G ) = Z )
cantnf.f 
|- F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
Assertion cantnflem3 
|- ( ph -> C e. ran ( A CNF B ) )

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 oemapval.t 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 cantnf.c 
 |-  ( ph -> C e. ( A ^o B ) )
6 cantnf.s 
 |-  ( ph -> C C_ ran ( A CNF B ) )
7 cantnf.e 
 |-  ( ph -> (/) e. C )
8 cantnf.x 
 |-  X = U. |^| { c e. On | C e. ( A ^o c ) }
9 cantnf.p 
 |-  P = ( iota d E. a e. On E. b e. ( A ^o X ) ( d = <. a , b >. /\ ( ( ( A ^o X ) .o a ) +o b ) = C ) )
10 cantnf.y 
 |-  Y = ( 1st ` P )
11 cantnf.z 
 |-  Z = ( 2nd ` P )
12 cantnf.g 
 |-  ( ph -> G e. S )
13 cantnf.v 
 |-  ( ph -> ( ( A CNF B ) ` G ) = Z )
14 cantnf.f 
 |-  F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
15 1 2 3 4 5 6 7 cantnflem2 
 |-  ( ph -> ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) )
16 eqid 
 |-  X = X
17 eqid 
 |-  Y = Y
18 eqid 
 |-  Z = Z
19 16 17 18 3pm3.2i 
 |-  ( X = X /\ Y = Y /\ Z = Z )
20 8 9 10 11 oeeui 
 |-  ( ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) -> ( ( ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) /\ ( ( ( A ^o X ) .o Y ) +o Z ) = C ) <-> ( X = X /\ Y = Y /\ Z = Z ) ) )
21 19 20 mpbiri 
 |-  ( ( A e. ( On \ 2o ) /\ C e. ( On \ 1o ) ) -> ( ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) /\ ( ( ( A ^o X ) .o Y ) +o Z ) = C ) )
22 15 21 syl 
 |-  ( ph -> ( ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) /\ ( ( ( A ^o X ) .o Y ) +o Z ) = C ) )
23 22 simpld 
 |-  ( ph -> ( X e. On /\ Y e. ( A \ 1o ) /\ Z e. ( A ^o X ) ) )
24 23 simp1d 
 |-  ( ph -> X e. On )
25 oecl 
 |-  ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On )
26 2 24 25 syl2anc 
 |-  ( ph -> ( A ^o X ) e. On )
27 23 simp2d 
 |-  ( ph -> Y e. ( A \ 1o ) )
28 27 eldifad 
 |-  ( ph -> Y e. A )
29 onelon 
 |-  ( ( A e. On /\ Y e. A ) -> Y e. On )
30 2 28 29 syl2anc 
 |-  ( ph -> Y e. On )
31 dif1o 
 |-  ( Y e. ( A \ 1o ) <-> ( Y e. A /\ Y =/= (/) ) )
32 31 simprbi 
 |-  ( Y e. ( A \ 1o ) -> Y =/= (/) )
33 27 32 syl 
 |-  ( ph -> Y =/= (/) )
34 on0eln0 
 |-  ( Y e. On -> ( (/) e. Y <-> Y =/= (/) ) )
35 30 34 syl 
 |-  ( ph -> ( (/) e. Y <-> Y =/= (/) ) )
36 33 35 mpbird 
 |-  ( ph -> (/) e. Y )
37 omword1 
 |-  ( ( ( ( A ^o X ) e. On /\ Y e. On ) /\ (/) e. Y ) -> ( A ^o X ) C_ ( ( A ^o X ) .o Y ) )
38 26 30 36 37 syl21anc 
 |-  ( ph -> ( A ^o X ) C_ ( ( A ^o X ) .o Y ) )
39 omcl 
 |-  ( ( ( A ^o X ) e. On /\ Y e. On ) -> ( ( A ^o X ) .o Y ) e. On )
40 26 30 39 syl2anc 
 |-  ( ph -> ( ( A ^o X ) .o Y ) e. On )
41 23 simp3d 
 |-  ( ph -> Z e. ( A ^o X ) )
42 onelon 
 |-  ( ( ( A ^o X ) e. On /\ Z e. ( A ^o X ) ) -> Z e. On )
43 26 41 42 syl2anc 
 |-  ( ph -> Z e. On )
44 oaword1 
 |-  ( ( ( ( A ^o X ) .o Y ) e. On /\ Z e. On ) -> ( ( A ^o X ) .o Y ) C_ ( ( ( A ^o X ) .o Y ) +o Z ) )
45 40 43 44 syl2anc 
 |-  ( ph -> ( ( A ^o X ) .o Y ) C_ ( ( ( A ^o X ) .o Y ) +o Z ) )
46 22 simprd 
 |-  ( ph -> ( ( ( A ^o X ) .o Y ) +o Z ) = C )
47 45 46 sseqtrd 
 |-  ( ph -> ( ( A ^o X ) .o Y ) C_ C )
48 38 47 sstrd 
 |-  ( ph -> ( A ^o X ) C_ C )
49 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
50 2 3 49 syl2anc 
 |-  ( ph -> ( A ^o B ) e. On )
51 ontr2 
 |-  ( ( ( A ^o X ) e. On /\ ( A ^o B ) e. On ) -> ( ( ( A ^o X ) C_ C /\ C e. ( A ^o B ) ) -> ( A ^o X ) e. ( A ^o B ) ) )
52 26 50 51 syl2anc 
 |-  ( ph -> ( ( ( A ^o X ) C_ C /\ C e. ( A ^o B ) ) -> ( A ^o X ) e. ( A ^o B ) ) )
53 48 5 52 mp2and 
 |-  ( ph -> ( A ^o X ) e. ( A ^o B ) )
54 15 simpld 
 |-  ( ph -> A e. ( On \ 2o ) )
55 oeord 
 |-  ( ( X e. On /\ B e. On /\ A e. ( On \ 2o ) ) -> ( X e. B <-> ( A ^o X ) e. ( A ^o B ) ) )
56 24 3 54 55 syl3anc 
 |-  ( ph -> ( X e. B <-> ( A ^o X ) e. ( A ^o B ) ) )
57 53 56 mpbird 
 |-  ( ph -> X e. B )
58 2 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> A e. On )
59 3 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> B e. On )
60 suppssdm 
 |-  ( G supp (/) ) C_ dom G
61 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
62 12 61 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
63 62 simpld 
 |-  ( ph -> G : B --> A )
64 60 63 fssdm 
 |-  ( ph -> ( G supp (/) ) C_ B )
65 64 sselda 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> x e. B )
66 onelon 
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
67 59 65 66 syl2anc 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> x e. On )
68 oecl 
 |-  ( ( A e. On /\ x e. On ) -> ( A ^o x ) e. On )
69 58 67 68 syl2anc 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( A ^o x ) e. On )
70 63 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> G : B --> A )
71 70 65 ffvelcdmd 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( G ` x ) e. A )
72 onelon 
 |-  ( ( A e. On /\ ( G ` x ) e. A ) -> ( G ` x ) e. On )
73 58 71 72 syl2anc 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( G ` x ) e. On )
74 63 ffnd 
 |-  ( ph -> G Fn B )
75 7 elexd 
 |-  ( ph -> (/) e. _V )
76 elsuppfn 
 |-  ( ( G Fn B /\ B e. On /\ (/) e. _V ) -> ( x e. ( G supp (/) ) <-> ( x e. B /\ ( G ` x ) =/= (/) ) ) )
77 74 3 75 76 syl3anc 
 |-  ( ph -> ( x e. ( G supp (/) ) <-> ( x e. B /\ ( G ` x ) =/= (/) ) ) )
78 77 simplbda 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( G ` x ) =/= (/) )
79 on0eln0 
 |-  ( ( G ` x ) e. On -> ( (/) e. ( G ` x ) <-> ( G ` x ) =/= (/) ) )
80 73 79 syl 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( (/) e. ( G ` x ) <-> ( G ` x ) =/= (/) ) )
81 78 80 mpbird 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> (/) e. ( G ` x ) )
82 omword1 
 |-  ( ( ( ( A ^o x ) e. On /\ ( G ` x ) e. On ) /\ (/) e. ( G ` x ) ) -> ( A ^o x ) C_ ( ( A ^o x ) .o ( G ` x ) ) )
83 69 73 81 82 syl21anc 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( A ^o x ) C_ ( ( A ^o x ) .o ( G ` x ) ) )
84 eqid 
 |-  OrdIso ( _E , ( G supp (/) ) ) = OrdIso ( _E , ( G supp (/) ) )
85 12 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> G e. S )
86 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) .o ( G ` ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) .o ( G ` ( OrdIso ( _E , ( G supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
87 1 58 59 84 85 86 65 cantnfle 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( ( A ^o x ) .o ( G ` x ) ) C_ ( ( A CNF B ) ` G ) )
88 13 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( ( A CNF B ) ` G ) = Z )
89 87 88 sseqtrd 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( ( A ^o x ) .o ( G ` x ) ) C_ Z )
90 83 89 sstrd 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( A ^o x ) C_ Z )
91 41 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> Z e. ( A ^o X ) )
92 26 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( A ^o X ) e. On )
93 ontr2 
 |-  ( ( ( A ^o x ) e. On /\ ( A ^o X ) e. On ) -> ( ( ( A ^o x ) C_ Z /\ Z e. ( A ^o X ) ) -> ( A ^o x ) e. ( A ^o X ) ) )
94 69 92 93 syl2anc 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( ( ( A ^o x ) C_ Z /\ Z e. ( A ^o X ) ) -> ( A ^o x ) e. ( A ^o X ) ) )
95 90 91 94 mp2and 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( A ^o x ) e. ( A ^o X ) )
96 24 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> X e. On )
97 54 adantr 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> A e. ( On \ 2o ) )
98 oeord 
 |-  ( ( x e. On /\ X e. On /\ A e. ( On \ 2o ) ) -> ( x e. X <-> ( A ^o x ) e. ( A ^o X ) ) )
99 67 96 97 98 syl3anc 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> ( x e. X <-> ( A ^o x ) e. ( A ^o X ) ) )
100 95 99 mpbird 
 |-  ( ( ph /\ x e. ( G supp (/) ) ) -> x e. X )
101 100 ex 
 |-  ( ph -> ( x e. ( G supp (/) ) -> x e. X ) )
102 101 ssrdv 
 |-  ( ph -> ( G supp (/) ) C_ X )
103 1 2 3 12 57 28 102 14 cantnfp1 
 |-  ( ph -> ( F e. S /\ ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) ) )
104 103 simprd 
 |-  ( ph -> ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )
105 13 oveq2d 
 |-  ( ph -> ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) = ( ( ( A ^o X ) .o Y ) +o Z ) )
106 104 105 46 3eqtrd 
 |-  ( ph -> ( ( A CNF B ) ` F ) = C )
107 1 2 3 cantnff 
 |-  ( ph -> ( A CNF B ) : S --> ( A ^o B ) )
108 107 ffnd 
 |-  ( ph -> ( A CNF B ) Fn S )
109 103 simpld 
 |-  ( ph -> F e. S )
110 fnfvelrn 
 |-  ( ( ( A CNF B ) Fn S /\ F e. S ) -> ( ( A CNF B ) ` F ) e. ran ( A CNF B ) )
111 108 109 110 syl2anc 
 |-  ( ph -> ( ( A CNF B ) ` F ) e. ran ( A CNF B ) )
112 106 111 eqeltrrd 
 |-  ( ph -> C e. ran ( A CNF B ) )