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

Metamath Proof Explorer

Theorem cantnflem3

Proof