cantnflt

Description: An upper bound on the partial sums of the CNF function. Since each term dominates all previous terms, by induction we can bound the whole sum with any exponent A ^o C where C is larger than any exponent ( Gx ) , x e. K which has been summed so far. (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 29-Jun-2019)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnfcl.g	$⊢ G = OrdIso (E, F supp \emptyset)$
	cantnfcl.f	$⊢ φ \to F \in S$
	cantnfval.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
	cantnflt.a	$⊢ φ \to \emptyset \in A$
	cantnflt.k	$⊢ φ \to K \in suc dom G$
	cantnflt.c	$⊢ φ \to C \in On$
	cantnflt.s	$⊢ φ \to G [K] \subseteq C$
Assertion	cantnflt	$⊢ φ \to H (K) \in (A ↑_{𝑜} C)$

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		cantnfcl.g	$⊢ G = OrdIso (E, F supp \emptyset)$
5		cantnfcl.f	$⊢ φ \to F \in S$
6		cantnfval.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
7		cantnflt.a	$⊢ φ \to \emptyset \in A$
8		cantnflt.k	$⊢ φ \to K \in suc dom G$
9		cantnflt.c	$⊢ φ \to C \in On$
10		cantnflt.s	$⊢ φ \to G [K] \subseteq C$
11		oen0	$⊢ ((A \in On \land C \in On) \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} C)$
12	2 9 7 11	syl21anc	$⊢ φ \to \emptyset \in (A ↑_{𝑜} C)$
13		fveq2	$⊢ K = \emptyset \to H (K) = H (\emptyset)$
14		0ex	$⊢ \emptyset \in V$
15	6	seqom0g	$⊢ \emptyset \in V \to H (\emptyset) = \emptyset$
16	14 15	ax-mp	$⊢ H (\emptyset) = \emptyset$
17	13 16	eqtrdi	$⊢ K = \emptyset \to H (K) = \emptyset$
18	17	eleq1d	$⊢ K = \emptyset \to (H (K) \in (A ↑_{𝑜} C) \leftrightarrow \emptyset \in (A ↑_{𝑜} C))$
19	12 18	syl5ibrcom	$⊢ φ \to (K = \emptyset \to H (K) \in (A ↑_{𝑜} C))$
20	9	adantr	$⊢ (φ \land (x \in ω \land K = suc x)) \to C \in On$
21		eloni	$⊢ C \in On \to Ord C$
22	20 21	syl	$⊢ (φ \land (x \in ω \land K = suc x)) \to Ord C$
23	10	adantr	$⊢ (φ \land (x \in ω \land K = suc x)) \to G [K] \subseteq C$
24	4	oif	$⊢ G : dom G ⟶ F supp \emptyset$
25		ffn	$⊢ G : dom G ⟶ F supp \emptyset \to G Fn dom G$
26	24 25	mp1i	$⊢ (φ \land (x \in ω \land K = suc x)) \to G Fn dom G$
27	4	oicl	$⊢ Ord dom G$
28		ordsuc	$⊢ Ord dom G \leftrightarrow Ord suc dom G$
29	27 28	mpbi	$⊢ Ord suc dom G$
30		ordelon	$⊢ (Ord suc dom G \land K \in suc dom G) \to K \in On$
31	29 8 30	sylancr	$⊢ φ \to K \in On$
32		ordsssuc	$⊢ (K \in On \land Ord dom G) \to (K \subseteq dom G \leftrightarrow K \in suc dom G)$
33	31 27 32	sylancl	$⊢ φ \to (K \subseteq dom G \leftrightarrow K \in suc dom G)$
34	8 33	mpbird	$⊢ φ \to K \subseteq dom G$
35	34	adantr	$⊢ (φ \land (x \in ω \land K = suc x)) \to K \subseteq dom G$
36		vex	$⊢ x \in V$
37	36	sucid	$⊢ x \in suc x$
38		simprr	$⊢ (φ \land (x \in ω \land K = suc x)) \to K = suc x$
39	37 38	eleqtrrid	$⊢ (φ \land (x \in ω \land K = suc x)) \to x \in K$
40		fnfvima	$⊢ (G Fn dom G \land K \subseteq dom G \land x \in K) \to G (x) \in G [K]$
41	26 35 39 40	syl3anc	$⊢ (φ \land (x \in ω \land K = suc x)) \to G (x) \in G [K]$
42	23 41	sseldd	$⊢ (φ \land (x \in ω \land K = suc x)) \to G (x) \in C$
43		ordsucss	$⊢ Ord C \to (G (x) \in C \to suc G (x) \subseteq C)$
44	22 42 43	sylc	$⊢ (φ \land (x \in ω \land K = suc x)) \to suc G (x) \subseteq C$
45		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
46	1 2 3	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$
47	5 46	mpbid	$⊢ φ \to (F : B ⟶ A \land {finSupp}_{\emptyset} (F))$
48	47	simpld	$⊢ φ \to F : B ⟶ A$
49	45 48	fssdm	$⊢ φ \to F supp \emptyset \subseteq B$
50		onss	$⊢ B \in On \to B \subseteq On$
51	3 50	syl	$⊢ φ \to B \subseteq On$
52	49 51	sstrd	$⊢ φ \to F supp \emptyset \subseteq On$
53	52	adantr	$⊢ (φ \land (x \in ω \land K = suc x)) \to F supp \emptyset \subseteq On$
54	8	adantr	$⊢ (φ \land (x \in ω \land K = suc x)) \to K \in suc dom G$
55	38 54	eqeltrrd	$⊢ (φ \land (x \in ω \land K = suc x)) \to suc x \in suc dom G$
56		ordsucelsuc	$⊢ Ord dom G \to (x \in dom G \leftrightarrow suc x \in suc dom G)$
57	27 56	ax-mp	$⊢ x \in dom G \leftrightarrow suc x \in suc dom G$
58	55 57	sylibr	$⊢ (φ \land (x \in ω \land K = suc x)) \to x \in dom G$
59	24	ffvelrni	$⊢ x \in dom G \to G (x) \in {supp}_{\emptyset} (F)$
60	58 59	syl	$⊢ (φ \land (x \in ω \land K = suc x)) \to G (x) \in {supp}_{\emptyset} (F)$
61	53 60	sseldd	$⊢ (φ \land (x \in ω \land K = suc x)) \to G (x) \in On$
62		suceloni	$⊢ G (x) \in On \to suc G (x) \in On$
63	61 62	syl	$⊢ (φ \land (x \in ω \land K = suc x)) \to suc G (x) \in On$
64	2	adantr	$⊢ (φ \land (x \in ω \land K = suc x)) \to A \in On$
65	7	adantr	$⊢ (φ \land (x \in ω \land K = suc x)) \to \emptyset \in A$
66		oewordi	$⊢ ((suc G (x) \in On \land C \in On \land A \in On) \land \emptyset \in A) \to (suc G (x) \subseteq C \to A ↑_{𝑜} suc G (x) \subseteq A ↑_{𝑜} C)$
67	63 20 64 65 66	syl31anc	$⊢ (φ \land (x \in ω \land K = suc x)) \to (suc G (x) \subseteq C \to A ↑_{𝑜} suc G (x) \subseteq A ↑_{𝑜} C)$
68	44 67	mpd	$⊢ (φ \land (x \in ω \land K = suc x)) \to A ↑_{𝑜} suc G (x) \subseteq A ↑_{𝑜} C$
69	38	fveq2d	$⊢ (φ \land (x \in ω \land K = suc x)) \to H (K) = H (suc x)$
70		simprl	$⊢ (φ \land (x \in ω \land K = suc x)) \to x \in ω$
71		simpl	$⊢ (φ \land (x \in ω \land K = suc x)) \to φ$
72		eleq1	$⊢ x = \emptyset \to (x \in dom G \leftrightarrow \emptyset \in dom G)$
73		suceq	$⊢ x = \emptyset \to suc x = suc \emptyset$
74	73	fveq2d	$⊢ x = \emptyset \to H (suc x) = H (suc \emptyset)$
75		fveq2	$⊢ x = \emptyset \to G (x) = G (\emptyset)$
76		suceq	$⊢ G (x) = G (\emptyset) \to suc G (x) = suc G (\emptyset)$
77	75 76	syl	$⊢ x = \emptyset \to suc G (x) = suc G (\emptyset)$
78	77	oveq2d	$⊢ x = \emptyset \to A ↑_{𝑜} suc G (x) = A ↑_{𝑜} suc G (\emptyset)$
79	74 78	eleq12d	$⊢ x = \emptyset \to (H (suc x) \in (A ↑_{𝑜} suc G (x)) \leftrightarrow H (suc \emptyset) \in (A ↑_{𝑜} suc G (\emptyset)))$
80	72 79	imbi12d	$⊢ x = \emptyset \to ((x \in dom G \to H (suc x) \in (A ↑_{𝑜} suc G (x))) \leftrightarrow (\emptyset \in dom G \to H (suc \emptyset) \in (A ↑_{𝑜} suc G (\emptyset))))$
81		eleq1	$⊢ x = y \to (x \in dom G \leftrightarrow y \in dom G)$
82		suceq	$⊢ x = y \to suc x = suc y$
83	82	fveq2d	$⊢ x = y \to H (suc x) = H (suc y)$
84		fveq2	$⊢ x = y \to G (x) = G (y)$
85		suceq	$⊢ G (x) = G (y) \to suc G (x) = suc G (y)$
86	84 85	syl	$⊢ x = y \to suc G (x) = suc G (y)$
87	86	oveq2d	$⊢ x = y \to A ↑_{𝑜} suc G (x) = A ↑_{𝑜} suc G (y)$
88	83 87	eleq12d	$⊢ x = y \to (H (suc x) \in (A ↑_{𝑜} suc G (x)) \leftrightarrow H (suc y) \in (A ↑_{𝑜} suc G (y)))$
89	81 88	imbi12d	$⊢ x = y \to ((x \in dom G \to H (suc x) \in (A ↑_{𝑜} suc G (x))) \leftrightarrow (y \in dom G \to H (suc y) \in (A ↑_{𝑜} suc G (y))))$
90		eleq1	$⊢ x = suc y \to (x \in dom G \leftrightarrow suc y \in dom G)$
91		suceq	$⊢ x = suc y \to suc x = suc suc y$
92	91	fveq2d	$⊢ x = suc y \to H (suc x) = H (suc suc y)$
93		fveq2	$⊢ x = suc y \to G (x) = G (suc y)$
94		suceq	$⊢ G (x) = G (suc y) \to suc G (x) = suc G (suc y)$
95	93 94	syl	$⊢ x = suc y \to suc G (x) = suc G (suc y)$
96	95	oveq2d	$⊢ x = suc y \to A ↑_{𝑜} suc G (x) = A ↑_{𝑜} suc G (suc y)$
97	92 96	eleq12d	$⊢ x = suc y \to (H (suc x) \in (A ↑_{𝑜} suc G (x)) \leftrightarrow H (suc suc y) \in (A ↑_{𝑜} suc G (suc y)))$
98	90 97	imbi12d	$⊢ x = suc y \to ((x \in dom G \to H (suc x) \in (A ↑_{𝑜} suc G (x))) \leftrightarrow (suc y \in dom G \to H (suc suc y) \in (A ↑_{𝑜} suc G (suc y))))$
99	48	adantr	$⊢ (φ \land \emptyset \in dom G) \to F : B ⟶ A$
100	24	ffvelrni	$⊢ \emptyset \in dom G \to G (\emptyset) \in {supp}_{\emptyset} (F)$
101	49	sselda	$⊢ (φ \land G (\emptyset) \in {supp}_{\emptyset} (F)) \to G (\emptyset) \in B$
102	100 101	sylan2	$⊢ (φ \land \emptyset \in dom G) \to G (\emptyset) \in B$
103	99 102	ffvelrnd	$⊢ (φ \land \emptyset \in dom G) \to F (G (\emptyset)) \in A$
104	2	adantr	$⊢ (φ \land \emptyset \in dom G) \to A \in On$
105		onelon	$⊢ (A \in On \land F (G (\emptyset)) \in A) \to F (G (\emptyset)) \in On$
106	104 103 105	syl2anc	$⊢ (φ \land \emptyset \in dom G) \to F (G (\emptyset)) \in On$
107	52	sselda	$⊢ (φ \land G (\emptyset) \in {supp}_{\emptyset} (F)) \to G (\emptyset) \in On$
108	100 107	sylan2	$⊢ (φ \land \emptyset \in dom G) \to G (\emptyset) \in On$
109		oecl	$⊢ (A \in On \land G (\emptyset) \in On) \to A ↑_{𝑜} G (\emptyset) \in On$
110	104 108 109	syl2anc	$⊢ (φ \land \emptyset \in dom G) \to A ↑_{𝑜} G (\emptyset) \in On$
111	7	adantr	$⊢ (φ \land \emptyset \in dom G) \to \emptyset \in A$
112		oen0	$⊢ ((A \in On \land G (\emptyset) \in On) \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} G (\emptyset))$
113	104 108 111 112	syl21anc	$⊢ (φ \land \emptyset \in dom G) \to \emptyset \in (A ↑_{𝑜} G (\emptyset))$
114		omord2	$⊢ ((F (G (\emptyset)) \in On \land A \in On \land A ↑_{𝑜} G (\emptyset) \in On) \land \emptyset \in (A ↑_{𝑜} G (\emptyset))) \to (F (G (\emptyset)) \in A \leftrightarrow (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)) \in ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} A))$
115	106 104 110 113 114	syl31anc	$⊢ (φ \land \emptyset \in dom G) \to (F (G (\emptyset)) \in A \leftrightarrow (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)) \in ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} A))$
116	103 115	mpbid	$⊢ (φ \land \emptyset \in dom G) \to (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)) \in ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} A)$
117		peano1	$⊢ \emptyset \in ω$
118	117	a1i	$⊢ \emptyset \in dom G \to \emptyset \in ω$
119	1 2 3 4 5 6	cantnfsuc	$⊢ (φ \land \emptyset \in ω) \to H (suc \emptyset) = ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))) +_{𝑜} H (\emptyset)$
120	118 119	sylan2	$⊢ (φ \land \emptyset \in dom G) \to H (suc \emptyset) = ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))) +_{𝑜} H (\emptyset)$
121	16	oveq2i	$⊢ ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))) +_{𝑜} H (\emptyset) = ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))) +_{𝑜} \emptyset$
122		omcl	$⊢ (A ↑_{𝑜} G (\emptyset) \in On \land F (G (\emptyset)) \in On) \to (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)) \in On$
123	110 106 122	syl2anc	$⊢ (φ \land \emptyset \in dom G) \to (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)) \in On$
124		oa0	$⊢ (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset)) \in On \to ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))) +_{𝑜} \emptyset = (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))$
125	123 124	syl	$⊢ (φ \land \emptyset \in dom G) \to ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))) +_{𝑜} \emptyset = (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))$
126	121 125	eqtrid	$⊢ (φ \land \emptyset \in dom G) \to ((A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))) +_{𝑜} H (\emptyset) = (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))$
127	120 126	eqtrd	$⊢ (φ \land \emptyset \in dom G) \to H (suc \emptyset) = (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} F (G (\emptyset))$
128		oesuc	$⊢ (A \in On \land G (\emptyset) \in On) \to A ↑_{𝑜} suc G (\emptyset) = (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} A$
129	104 108 128	syl2anc	$⊢ (φ \land \emptyset \in dom G) \to A ↑_{𝑜} suc G (\emptyset) = (A ↑_{𝑜} G (\emptyset)) \cdot_{𝑜} A$
130	116 127 129	3eltr4d	$⊢ (φ \land \emptyset \in dom G) \to H (suc \emptyset) \in (A ↑_{𝑜} suc G (\emptyset))$
131	130	ex	$⊢ φ \to (\emptyset \in dom G \to H (suc \emptyset) \in (A ↑_{𝑜} suc G (\emptyset)))$
132		ordtr	$⊢ Ord dom G \to Tr dom G$
133	27 132	ax-mp	$⊢ Tr dom G$
134		trsuc	$⊢ (Tr dom G \land suc y \in dom G) \to y \in dom G$
135	133 134	mpan	$⊢ suc y \in dom G \to y \in dom G$
136	135	imim1i	$⊢ (y \in dom G \to H (suc y) \in (A ↑_{𝑜} suc G (y))) \to (suc y \in dom G \to H (suc y) \in (A ↑_{𝑜} suc G (y)))$
137	2	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to A \in On$
138		eloni	$⊢ A \in On \to Ord A$
139	137 138	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to Ord A$
140	48	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to F : B ⟶ A$
141	49	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to F supp \emptyset \subseteq B$
142	24	ffvelrni	$⊢ suc y \in dom G \to G (suc y) \in {supp}_{\emptyset} (F)$
143	142	ad2antrl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G (suc y) \in {supp}_{\emptyset} (F)$
144	141 143	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G (suc y) \in B$
145	140 144	ffvelrnd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to F (G (suc y)) \in A$
146		ordsucss	$⊢ Ord A \to (F (G (suc y)) \in A \to suc F (G (suc y)) \subseteq A)$
147	139 145 146	sylc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to suc F (G (suc y)) \subseteq A$
148		onelon	$⊢ (A \in On \land F (G (suc y)) \in A) \to F (G (suc y)) \in On$
149	137 145 148	syl2anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to F (G (suc y)) \in On$
150		suceloni	$⊢ F (G (suc y)) \in On \to suc F (G (suc y)) \in On$
151	149 150	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to suc F (G (suc y)) \in On$
152	52	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to F supp \emptyset \subseteq On$
153	152 143	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G (suc y) \in On$
154		oecl	$⊢ (A \in On \land G (suc y) \in On) \to A ↑_{𝑜} G (suc y) \in On$
155	137 153 154	syl2anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to A ↑_{𝑜} G (suc y) \in On$
156		omwordi	$⊢ (suc F (G (suc y)) \in On \land A \in On \land A ↑_{𝑜} G (suc y) \in On) \to (suc F (G (suc y)) \subseteq A \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} suc F (G (suc y)) \subseteq (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} A)$
157	151 137 155 156	syl3anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (suc F (G (suc y)) \subseteq A \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} suc F (G (suc y)) \subseteq (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} A)$
158	147 157	mpd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} suc F (G (suc y)) \subseteq (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} A$
159		oesuc	$⊢ (A \in On \land G (suc y) \in On) \to A ↑_{𝑜} suc G (suc y) = (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} A$
160	137 153 159	syl2anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to A ↑_{𝑜} suc G (suc y) = (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} A$
161	158 160	sseqtrrd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} suc F (G (suc y)) \subseteq A ↑_{𝑜} suc G (suc y)$
162		eloni	$⊢ G (suc y) \in On \to Ord G (suc y)$
163	153 162	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to Ord G (suc y)$
164		vex	$⊢ y \in V$
165	164	sucid	$⊢ y \in suc y$
166	164	sucex	$⊢ suc y \in V$
167	166	epeli	$⊢ y E suc y \leftrightarrow y \in suc y$
168	165 167	mpbir	$⊢ y E suc y$
169		ovexd	$⊢ φ \to F supp \emptyset \in V$
170	1 2 3 4 5	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$
171	170	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
172	4	oiiso	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
173	169 171 172	syl2anc	$⊢ φ \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
174	173	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
175	135	ad2antrl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to y \in dom G$
176		simprl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to suc y \in dom G$
177		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))$
178	174 175 176 177	syl12anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (y E suc y \leftrightarrow G (y) E G (suc y))$
179	168 178	mpbii	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G (y) E G (suc y)$
180		fvex	$⊢ G (suc y) \in V$
181	180	epeli	$⊢ G (y) E G (suc y) \leftrightarrow G (y) \in G (suc y)$
182	179 181	sylib	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G (y) \in G (suc y)$
183		ordsucss	$⊢ Ord G (suc y) \to (G (y) \in G (suc y) \to suc G (y) \subseteq G (suc y))$
184	163 182 183	sylc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to suc G (y) \subseteq G (suc y)$
185	24	ffvelrni	$⊢ y \in dom G \to G (y) \in {supp}_{\emptyset} (F)$
186	175 185	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G (y) \in {supp}_{\emptyset} (F)$
187	152 186	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to G (y) \in On$
188		suceloni	$⊢ G (y) \in On \to suc G (y) \in On$
189	187 188	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to suc G (y) \in On$
190	7	ad2antrr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to \emptyset \in A$
191		oewordi	$⊢ ((suc G (y) \in On \land G (suc y) \in On \land A \in On) \land \emptyset \in A) \to (suc G (y) \subseteq G (suc y) \to A ↑_{𝑜} suc G (y) \subseteq A ↑_{𝑜} G (suc y))$
192	189 153 137 190 191	syl31anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (suc G (y) \subseteq G (suc y) \to A ↑_{𝑜} suc G (y) \subseteq A ↑_{𝑜} G (suc y))$
193	184 192	mpd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to A ↑_{𝑜} suc G (y) \subseteq A ↑_{𝑜} G (suc y)$
194		simprr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to H (suc y) \in (A ↑_{𝑜} suc G (y))$
195	193 194	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to H (suc y) \in (A ↑_{𝑜} G (suc y))$
196		peano2	$⊢ y \in ω \to suc y \in ω$
197	196	ad2antlr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to suc y \in ω$
198	6	cantnfvalf	$⊢ H : ω ⟶ On$
199	198	ffvelrni	$⊢ suc y \in ω \to H (suc y) \in On$
200	197 199	syl	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to H (suc y) \in On$
201		omcl	$⊢ (A ↑_{𝑜} G (suc y) \in On \land F (G (suc y)) \in On) \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y)) \in On$
202	155 149 201	syl2anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y)) \in On$
203		oaord	$⊢ (H (suc y) \in On \land A ↑_{𝑜} G (suc y) \in On \land (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y)) \in On) \to (H (suc y) \in (A ↑_{𝑜} G (suc y)) \leftrightarrow ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} H (suc y) \in (((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} (A ↑_{𝑜} G (suc y))))$
204	200 155 202 203	syl3anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (H (suc y) \in (A ↑_{𝑜} G (suc y)) \leftrightarrow ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} H (suc y) \in (((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} (A ↑_{𝑜} G (suc y))))$
205	195 204	mpbid	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} H (suc y) \in (((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} (A ↑_{𝑜} G (suc y)))$
206	1 2 3 4 5 6	cantnfsuc	$⊢ (φ \land suc y \in ω) \to H (suc suc y) = ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} H (suc y)$
207	196 206	sylan2	$⊢ (φ \land y \in ω) \to H (suc suc y) = ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} H (suc y)$
208	207	adantr	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to H (suc suc y) = ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} H (suc y)$
209		omsuc	$⊢ (A ↑_{𝑜} G (suc y) \in On \land F (G (suc y)) \in On) \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} suc F (G (suc y)) = ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} (A ↑_{𝑜} G (suc y))$
210	155 149 209	syl2anc	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to (A ↑_{𝑜} G (suc y)) \cdot_{𝑜} suc F (G (suc y)) = ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} F (G (suc y))) +_{𝑜} (A ↑_{𝑜} G (suc y))$
211	205 208 210	3eltr4d	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to H (suc suc y) \in ((A ↑_{𝑜} G (suc y)) \cdot_{𝑜} suc F (G (suc y)))$
212	161 211	sseldd	$⊢ ((φ \land y \in ω) \land (suc y \in dom G \land H (suc y) \in (A ↑_{𝑜} suc G (y)))) \to H (suc suc y) \in (A ↑_{𝑜} suc G (suc y))$
213	212	exp32	$⊢ (φ \land y \in ω) \to (suc y \in dom G \to (H (suc y) \in (A ↑_{𝑜} suc G (y)) \to H (suc suc y) \in (A ↑_{𝑜} suc G (suc y))))$
214	213	a2d	$⊢ (φ \land y \in ω) \to ((suc y \in dom G \to H (suc y) \in (A ↑_{𝑜} suc G (y))) \to (suc y \in dom G \to H (suc suc y) \in (A ↑_{𝑜} suc G (suc y))))$
215	136 214	syl5	$⊢ (φ \land y \in ω) \to ((y \in dom G \to H (suc y) \in (A ↑_{𝑜} suc G (y))) \to (suc y \in dom G \to H (suc suc y) \in (A ↑_{𝑜} suc G (suc y))))$
216	215	expcom	$⊢ y \in ω \to (φ \to ((y \in dom G \to H (suc y) \in (A ↑_{𝑜} suc G (y))) \to (suc y \in dom G \to H (suc suc y) \in (A ↑_{𝑜} suc G (suc y)))))$
217	80 89 98 131 216	finds2	$⊢ x \in ω \to (φ \to (x \in dom G \to H (suc x) \in (A ↑_{𝑜} suc G (x))))$
218	70 71 58 217	syl3c	$⊢ (φ \land (x \in ω \land K = suc x)) \to H (suc x) \in (A ↑_{𝑜} suc G (x))$
219	69 218	eqeltrd	$⊢ (φ \land (x \in ω \land K = suc x)) \to H (K) \in (A ↑_{𝑜} suc G (x))$
220	68 219	sseldd	$⊢ (φ \land (x \in ω \land K = suc x)) \to H (K) \in (A ↑_{𝑜} C)$
221	220	rexlimdvaa	$⊢ φ \to (\exists x \in ω K = suc x \to H (K) \in (A ↑_{𝑜} C))$
222		peano2	$⊢ dom G \in ω \to suc dom G \in ω$
223	170 222	simpl2im	$⊢ φ \to suc dom G \in ω$
224		elnn	$⊢ (K \in suc dom G \land suc dom G \in ω) \to K \in ω$
225	8 223 224	syl2anc	$⊢ φ \to K \in ω$
226		nn0suc	$⊢ K \in ω \to (K = \emptyset \lor \exists x \in ω K = suc x)$
227	225 226	syl	$⊢ φ \to (K = \emptyset \lor \exists x \in ω K = suc x)$
228	19 221 227	mpjaod	$⊢ φ \to H (K) \in (A ↑_{𝑜} C)$

Metamath Proof Explorer

Theorem cantnflt

Proof