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	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
	cantnf.c	$⊢ φ \to C \in (A ↑_{𝑜} B)$
	cantnf.s	$⊢ φ \to C \subseteq ran (A CNF B)$
	cantnf.e	$⊢ φ \to \emptyset \in C$
	cantnf.x	$⊢ X = ⋃ ⋂ \{c \in On \| C \in (A ↑_{𝑜} c)\}$
	cantnf.p	$⊢ P = (ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} X) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} a) +_{𝑜} b = C))$
	cantnf.y	$⊢ Y = 1^{st} (P)$
	cantnf.z	$⊢ Z = 2^{nd} (P)$
	cantnf.g	$⊢ φ \to G \in S$
	cantnf.v	$⊢ φ \to (A CNF B) (G) = Z$
	cantnf.f	$⊢ F = (t \in B ⟼ if (t = X, Y, G (t)))$
Assertion	cantnflem3	$⊢ φ \to C \in ran (A CNF B)$

Proof

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

Metamath Proof Explorer

Theorem cantnflem3

Proof