cnfcom

Description: Any ordinal B is equinumerous to the leading term of its Cantor normal form. Here we show that bijection explicitly. (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	cnfcom.s	$⊢ S = dom (ω CNF A)$
	cnfcom.a	$⊢ φ \to A \in On$
	cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
	cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
	cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
	cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
	cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
	cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
	cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
	cnfcom.1	$⊢ φ \to I \in dom G$
Assertion	cnfcom	$⊢ φ \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$

Proof

Step	Hyp	Ref	Expression
1		cnfcom.s	$⊢ S = dom (ω CNF A)$
2		cnfcom.a	$⊢ φ \to A \in On$
3		cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
4		cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
5		cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
6		cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
7		cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
8		cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
9		cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
10		cnfcom.1	$⊢ φ \to I \in dom G$
11		omelon	$⊢ ω \in On$
12	11	a1i	$⊢ φ \to ω \in On$
13	1 12 2	cantnff1o	$⊢ φ \to (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A$
14		f1ocnv	$⊢ (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S$
15		f1of	$⊢ {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
16	13 14 15	3syl	$⊢ φ \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
17	16 3	ffvelcdmd	$⊢ φ \to {(ω CNF A)}^{-1} (B) \in S$
18	4 17	eqeltrid	$⊢ φ \to F \in S$
19	1 12 2 5 18	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$
20	19	simprd	$⊢ φ \to dom G \in ω$
21		elnn	$⊢ (I \in dom G \land dom G \in ω) \to I \in ω$
22	10 20 21	syl2anc	$⊢ φ \to I \in ω$
23		eleq1	$⊢ w = I \to (w \in dom G \leftrightarrow I \in dom G)$
24		suceq	$⊢ w = I \to suc w = suc I$
25	24	fveq2d	$⊢ w = I \to T (suc w) = T (suc I)$
26	24	fveq2d	$⊢ w = I \to H (suc w) = H (suc I)$
27		fveq2	$⊢ w = I \to G (w) = G (I)$
28	27	oveq2d	$⊢ w = I \to ω ↑_{𝑜} G (w) = ω ↑_{𝑜} G (I)$
29		2fveq3	$⊢ w = I \to F (G (w)) = F (G (I))$
30	28 29	oveq12d	$⊢ w = I \to (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) = (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$
31	25 26 30	f1oeq123d	$⊢ w = I \to (T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) \leftrightarrow T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))$
32	23 31	imbi12d	$⊢ w = I \to ((w \in dom G \to T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w))) \leftrightarrow (I \in dom G \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))))$
33	32	imbi2d	$⊢ w = I \to ((φ \to (w \in dom G \to T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)))) \leftrightarrow (φ \to (I \in dom G \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))))$
34		eleq1	$⊢ w = \emptyset \to (w \in dom G \leftrightarrow \emptyset \in dom G)$
35		suceq	$⊢ w = \emptyset \to suc w = suc \emptyset$
36	35	fveq2d	$⊢ w = \emptyset \to T (suc w) = T (suc \emptyset)$
37	35	fveq2d	$⊢ w = \emptyset \to H (suc w) = H (suc \emptyset)$
38		fveq2	$⊢ w = \emptyset \to G (w) = G (\emptyset)$
39	38	oveq2d	$⊢ w = \emptyset \to ω ↑_{𝑜} G (w) = ω ↑_{𝑜} G (\emptyset)$
40		2fveq3	$⊢ w = \emptyset \to F (G (w)) = F (G (\emptyset))$
41	39 40	oveq12d	$⊢ w = \emptyset \to (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) = (ω ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))$
42	36 37 41	f1oeq123d	$⊢ w = \emptyset \to (T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) \leftrightarrow T (suc \emptyset) : H (suc \emptyset) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)))$
43	34 42	imbi12d	$⊢ w = \emptyset \to ((w \in dom G \to T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w))) \leftrightarrow (\emptyset \in dom G \to T (suc \emptyset) : H (suc \emptyset) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))))$
44		eleq1	$⊢ w = y \to (w \in dom G \leftrightarrow y \in dom G)$
45		suceq	$⊢ w = y \to suc w = suc y$
46	45	fveq2d	$⊢ w = y \to T (suc w) = T (suc y)$
47	45	fveq2d	$⊢ w = y \to H (suc w) = H (suc y)$
48		fveq2	$⊢ w = y \to G (w) = G (y)$
49	48	oveq2d	$⊢ w = y \to ω ↑_{𝑜} G (w) = ω ↑_{𝑜} G (y)$
50		2fveq3	$⊢ w = y \to F (G (w)) = F (G (y))$
51	49 50	oveq12d	$⊢ w = y \to (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) = (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))$
52	46 47 51	f1oeq123d	$⊢ w = y \to (T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) \leftrightarrow T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))$
53	44 52	imbi12d	$⊢ w = y \to ((w \in dom G \to T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w))) \leftrightarrow (y \in dom G \to T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))))$
54		eleq1	$⊢ w = suc y \to (w \in dom G \leftrightarrow suc y \in dom G)$
55		suceq	$⊢ w = suc y \to suc w = suc suc y$
56	55	fveq2d	$⊢ w = suc y \to T (suc w) = T (suc suc y)$
57	55	fveq2d	$⊢ w = suc y \to H (suc w) = H (suc suc y)$
58		fveq2	$⊢ w = suc y \to G (w) = G (suc y)$
59	58	oveq2d	$⊢ w = suc y \to ω ↑_{𝑜} G (w) = ω ↑_{𝑜} G (suc y)$
60		2fveq3	$⊢ w = suc y \to F (G (w)) = F (G (suc y))$
61	59 60	oveq12d	$⊢ w = suc y \to (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) = (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))$
62	56 57 61	f1oeq123d	$⊢ w = suc y \to (T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w)) \leftrightarrow T (suc suc y) : H (suc suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y)))$
63	54 62	imbi12d	$⊢ w = suc y \to ((w \in dom G \to T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w))) \leftrightarrow (suc y \in dom G \to T (suc suc y) : H (suc suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))))$
64	2	adantr	$⊢ (φ \land \emptyset \in dom G) \to A \in On$
65	3	adantr	$⊢ (φ \land \emptyset \in dom G) \to B \in (ω ↑_{𝑜} A)$
66		simpr	$⊢ (φ \land \emptyset \in dom G) \to \emptyset \in dom G$
67	11	a1i	$⊢ (φ \land \emptyset \in dom G) \to ω \in On$
68		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
69	1 12 2	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : A ⟶ ω \land {finSupp}_{\emptyset} (F)))$
70	18 69	mpbid	$⊢ φ \to (F : A ⟶ ω \land {finSupp}_{\emptyset} (F))$
71	70	simpld	$⊢ φ \to F : A ⟶ ω$
72	68 71	fssdm	$⊢ φ \to F supp \emptyset \subseteq A$
73		onss	$⊢ A \in On \to A \subseteq On$
74	2 73	syl	$⊢ φ \to A \subseteq On$
75	72 74	sstrd	$⊢ φ \to F supp \emptyset \subseteq On$
76	5	oif	$⊢ G : dom G ⟶ F supp \emptyset$
77	76	ffvelcdmi	$⊢ \emptyset \in dom G \to G (\emptyset) \in {supp}_{\emptyset} (F)$
78		ssel2	$⊢ (F supp \emptyset \subseteq On \land G (\emptyset) \in {supp}_{\emptyset} (F)) \to G (\emptyset) \in On$
79	75 77 78	syl2an	$⊢ (φ \land \emptyset \in dom G) \to G (\emptyset) \in On$
80		peano1	$⊢ \emptyset \in ω$
81	80	a1i	$⊢ (φ \land \emptyset \in dom G) \to \emptyset \in ω$
82		oen0	$⊢ ((ω \in On \land G (\emptyset) \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} G (\emptyset))$
83	67 79 81 82	syl21anc	$⊢ (φ \land \emptyset \in dom G) \to \emptyset \in (ω ↑_{𝑜} G (\emptyset))$
84		0ex	$⊢ \emptyset \in V$
85	7	seqom0g	$⊢ \emptyset \in V \to T (\emptyset) = \emptyset$
86	84 85	ax-mp	$⊢ T (\emptyset) = \emptyset$
87		f1o0	$⊢ \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
88	6	seqom0g	$⊢ \emptyset \in V \to H (\emptyset) = \emptyset$
89		f1oeq2	$⊢ H (\emptyset) = \emptyset \to (\emptyset : H (\emptyset) \underset{1-1 onto}{⟶} \emptyset \leftrightarrow \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset)$
90	84 88 89	mp2b	$⊢ \emptyset : H (\emptyset) \underset{1-1 onto}{⟶} \emptyset \leftrightarrow \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
91	87 90	mpbir	$⊢ \emptyset : H (\emptyset) \underset{1-1 onto}{⟶} \emptyset$
92		f1oeq1	$⊢ T (\emptyset) = \emptyset \to (T (\emptyset) : H (\emptyset) \underset{1-1 onto}{⟶} \emptyset \leftrightarrow \emptyset : H (\emptyset) \underset{1-1 onto}{⟶} \emptyset)$
93	91 92	mpbiri	$⊢ T (\emptyset) = \emptyset \to T (\emptyset) : H (\emptyset) \underset{1-1 onto}{⟶} \emptyset$
94	86 93	mp1i	$⊢ (φ \land \emptyset \in dom G) \to T (\emptyset) : H (\emptyset) \underset{1-1 onto}{⟶} \emptyset$
95	1 64 65 4 5 6 7 8 9 66 83 94	cnfcomlem	$⊢ (φ \land \emptyset \in dom G) \to T (suc \emptyset) : H (suc \emptyset) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))$
96	95	ex	$⊢ φ \to (\emptyset \in dom G \to T (suc \emptyset) : H (suc \emptyset) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)))$
97	5	oicl	$⊢ Ord dom G$
98		ordtr	$⊢ Ord dom G \to Tr dom G$
99	97 98	ax-mp	$⊢ Tr dom G$
100		trsuc	$⊢ (Tr dom G \land suc y \in dom G) \to y \in dom G$
101	99 100	mpan	$⊢ suc y \in dom G \to y \in dom G$
102	101	imim1i	$⊢ (y \in dom G \to T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) \to (suc y \in dom G \to T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))$
103	2	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to A \in On$
104	3	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to B \in (ω ↑_{𝑜} A)$
105		simprl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to suc y \in dom G$
106	74	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to A \subseteq On$
107	72	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to F supp \emptyset \subseteq A$
108	76	ffvelcdmi	$⊢ suc y \in dom G \to G (suc y) \in {supp}_{\emptyset} (F)$
109	108	ad2antrl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G (suc y) \in {supp}_{\emptyset} (F)$
110	107 109	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G (suc y) \in A$
111	106 110	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G (suc y) \in On$
112		eloni	$⊢ G (suc y) \in On \to Ord G (suc y)$
113	111 112	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to Ord G (suc y)$
114		vex	$⊢ y \in V$
115	114	sucid	$⊢ y \in suc y$
116		ovexd	$⊢ φ \to F supp \emptyset \in V$
117	19	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
118	5	oiiso	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
119	116 117 118	syl2anc	$⊢ φ \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
120	119	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
121	101	ad2antrl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to y \in dom G$
122		isorel	$⊢ (G {Isom}_{E, E} (dom G, F supp \emptyset) \land (y \in dom G \land suc y \in dom G)) \to (y E suc y \leftrightarrow G (y) E G (suc y))$
123	120 121 105 122	syl12anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to (y E suc y \leftrightarrow G (y) E G (suc y))$
124	114	sucex	$⊢ suc y \in V$
125	124	epeli	$⊢ y E suc y \leftrightarrow y \in suc y$
126		fvex	$⊢ G (suc y) \in V$
127	126	epeli	$⊢ G (y) E G (suc y) \leftrightarrow G (y) \in G (suc y)$
128	123 125 127	3bitr3g	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to (y \in suc y \leftrightarrow G (y) \in G (suc y))$
129	115 128	mpbii	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G (y) \in G (suc y)$
130		ordsucss	$⊢ Ord G (suc y) \to (G (y) \in G (suc y) \to suc G (y) \subseteq G (suc y))$
131	113 129 130	sylc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to suc G (y) \subseteq G (suc y)$
132	76	ffvelcdmi	$⊢ y \in dom G \to G (y) \in {supp}_{\emptyset} (F)$
133	121 132	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G (y) \in {supp}_{\emptyset} (F)$
134	107 133	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G (y) \in A$
135	106 134	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to G (y) \in On$
136		onsuc	$⊢ G (y) \in On \to suc G (y) \in On$
137	135 136	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to suc G (y) \in On$
138	11	a1i	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to ω \in On$
139	80	a1i	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to \emptyset \in ω$
140		oewordi	$⊢ ((suc G (y) \in On \land G (suc y) \in On \land ω \in On) \land \emptyset \in ω) \to (suc G (y) \subseteq G (suc y) \to ω ↑_{𝑜} suc G (y) \subseteq ω ↑_{𝑜} G (suc y))$
141	137 111 138 139 140	syl31anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to (suc G (y) \subseteq G (suc y) \to ω ↑_{𝑜} suc G (y) \subseteq ω ↑_{𝑜} G (suc y))$
142	131 141	mpd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to ω ↑_{𝑜} suc G (y) \subseteq ω ↑_{𝑜} G (suc y)$
143	71	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to F : A ⟶ ω$
144	143 134	ffvelcdmd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to F (G (y)) \in ω$
145		nnon	$⊢ F (G (y)) \in ω \to F (G (y)) \in On$
146	144 145	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to F (G (y)) \in On$
147		oecl	$⊢ (ω \in On \land G (y) \in On) \to ω ↑_{𝑜} G (y) \in On$
148	138 135 147	syl2anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to ω ↑_{𝑜} G (y) \in On$
149		oen0	$⊢ ((ω \in On \land G (y) \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} G (y))$
150	138 135 139 149	syl21anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to \emptyset \in (ω ↑_{𝑜} G (y))$
151		omord2	$⊢ ((F (G (y)) \in On \land ω \in On \land ω ↑_{𝑜} G (y) \in On) \land \emptyset \in (ω ↑_{𝑜} G (y))) \to (F (G (y)) \in ω \leftrightarrow (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in ((ω ↑_{𝑜} G (y)) \cdot_{𝑜} ω))$
152	146 138 148 150 151	syl31anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to (F (G (y)) \in ω \leftrightarrow (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in ((ω ↑_{𝑜} G (y)) \cdot_{𝑜} ω))$
153	144 152	mpbid	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in ((ω ↑_{𝑜} G (y)) \cdot_{𝑜} ω)$
154		oesuc	$⊢ (ω \in On \land G (y) \in On) \to ω ↑_{𝑜} suc G (y) = (ω ↑_{𝑜} G (y)) \cdot_{𝑜} ω$
155	138 135 154	syl2anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to ω ↑_{𝑜} suc G (y) = (ω ↑_{𝑜} G (y)) \cdot_{𝑜} ω$
156	153 155	eleqtrrd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in (ω ↑_{𝑜} suc G (y))$
157	142 156	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in (ω ↑_{𝑜} G (suc y))$
158		simprr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))$
159	1 103 104 4 5 6 7 8 9 105 157 158	cnfcomlem	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)))) \to T (suc suc y) : H (suc suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))$
160	159	exp32	$⊢ (φ \land y \in ω) \to (suc y \in dom G \to (T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \to T (suc suc y) : H (suc suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))))$
161	160	a2d	$⊢ (φ \land y \in ω) \to ((suc y \in dom G \to T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) \to (suc y \in dom G \to T (suc suc y) : H (suc suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))))$
162	102 161	syl5	$⊢ (φ \land y \in ω) \to ((y \in dom G \to T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) \to (suc y \in dom G \to T (suc suc y) : H (suc suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))))$
163	162	expcom	$⊢ y \in ω \to (φ \to ((y \in dom G \to T (suc y) : H (suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) \to (suc y \in dom G \to T (suc suc y) : H (suc suc y) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y)))))$
164	43 53 63 96 163	finds2	$⊢ w \in ω \to (φ \to (w \in dom G \to T (suc w) : H (suc w) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (w)) \cdot_{𝑜} F (G (w))))$
165	33 164	vtoclga	$⊢ I \in ω \to (φ \to (I \in dom G \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))))$
166	22 165	mpcom	$⊢ φ \to (I \in dom G \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))$
167	10 166	mpd	$⊢ φ \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$

Metamath Proof Explorer

Theorem cnfcom

Proof