Theorem cantnfle

Description: A lower bound on the CNF function. Since ( ( A CNF B )F ) is defined as the sum of ( A ^o x ) .o ( Fx ) over all x in the support of F , it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all C e. B instead of just those C in the support). (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 28-Jun-2019)

	Ref	Expression
Hypotheses	cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	cantnfcl.g	⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
	cantnfcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
	cantnfval.h	⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
	cantnfle.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion	cantnfle	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
4		cantnfcl.g	⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
5		cantnfcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6		cantnfval.h	⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
7		cantnfle.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
8		oveq2	⊢ ( ( 𝐹 ‘ 𝐶 ) = ∅ → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) = ( ( 𝐴 ↑o 𝐶 ) ·o ∅ ) )
9	8	sseq1d	⊢ ( ( 𝐹 ‘ 𝐶 ) = ∅ → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ↔ ( ( 𝐴 ↑o 𝐶 ) ·o ∅ ) ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ) )
10		ovexd	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
11	1 2 3 4 5	cantnfcl	⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )
12	11	simpld	⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
13	4	oiiso	⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
14	10 12 13	syl2anc	⊢ ( 𝜑 → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
15		isof1o	⊢ ( 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) → 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) )
16	14 15	syl	⊢ ( 𝜑 → 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) )
18		f1ocnv	⊢ ( 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) → ◡ 𝐺 : ( 𝐹 supp ∅ ) –1-1-onto→ dom 𝐺 )
19		f1of	⊢ ( ◡ 𝐺 : ( 𝐹 supp ∅ ) –1-1-onto→ dom 𝐺 → ◡ 𝐺 : ( 𝐹 supp ∅ ) ⟶ dom 𝐺 )
20	17 18 19	3syl	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ◡ 𝐺 : ( 𝐹 supp ∅ ) ⟶ dom 𝐺 )
21	7	anim1i	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( 𝐶 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) )
22	1 2 3	cantnfs	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
23	5 22	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) )
24	23	simpld	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → 𝐹 : 𝐵 ⟶ 𝐴 )
26	25	ffnd	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → 𝐹 Fn 𝐵 )
27	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → 𝐵 ∈ On )
28		0ex	⊢ ∅ ∈ V
29	28	a1i	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ∅ ∈ V )
30		elsuppfn	⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( 𝐶 ∈ ( 𝐹 supp ∅ ) ↔ ( 𝐶 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ) )
31	26 27 29 30	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( 𝐶 ∈ ( 𝐹 supp ∅ ) ↔ ( 𝐶 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ) )
32	21 31	mpbird	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → 𝐶 ∈ ( 𝐹 supp ∅ ) )
33	20 32	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ◡ 𝐺 ‘ 𝐶 ) ∈ dom 𝐺 )
34	11	simprd	⊢ ( 𝜑 → dom 𝐺 ∈ ω )
35	34	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → dom 𝐺 ∈ ω )
36		eqimss	⊢ ( 𝑥 = dom 𝐺 → 𝑥 ⊆ dom 𝐺 )
37	36	biantrurd	⊢ ( 𝑥 = dom 𝐺 → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ↔ ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) ) )
38		eleq2	⊢ ( 𝑥 = dom 𝐺 → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ↔ ( ◡ 𝐺 ‘ 𝐶 ) ∈ dom 𝐺 ) )
39	37 38	bitr3d	⊢ ( 𝑥 = dom 𝐺 → ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) ↔ ( ◡ 𝐺 ‘ 𝐶 ) ∈ dom 𝐺 ) )
40		fveq2	⊢ ( 𝑥 = dom 𝐺 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ dom 𝐺 ) )
41	40	sseq2d	⊢ ( 𝑥 = dom 𝐺 → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ↔ ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ dom 𝐺 ) ) )
42	39 41	imbi12d	⊢ ( 𝑥 = dom 𝐺 → ( ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ) ↔ ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ dom 𝐺 → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ dom 𝐺 ) ) ) )
43	42	imbi2d	⊢ ( 𝑥 = dom 𝐺 → ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ dom 𝐺 → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ dom 𝐺 ) ) ) ) )
44		sseq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ dom 𝐺 ↔ ∅ ⊆ dom 𝐺 ) )
45		eleq2	⊢ ( 𝑥 = ∅ → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ↔ ( ◡ 𝐺 ‘ 𝐶 ) ∈ ∅ ) )
46	44 45	anbi12d	⊢ ( 𝑥 = ∅ → ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) ↔ ( ∅ ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ ∅ ) ) )
47		fveq2	⊢ ( 𝑥 = ∅ → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ∅ ) )
48	47	sseq2d	⊢ ( 𝑥 = ∅ → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ↔ ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ ∅ ) ) )
49	46 48	imbi12d	⊢ ( 𝑥 = ∅ → ( ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ) ↔ ( ( ∅ ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ ∅ ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ ∅ ) ) ) )
50		sseq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ dom 𝐺 ↔ 𝑦 ⊆ dom 𝐺 ) )
51		eleq2	⊢ ( 𝑥 = 𝑦 → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ↔ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) )
52	50 51	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) ↔ ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) ) )
53		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) )
54	53	sseq2d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ↔ ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) )
55	52 54	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ) ↔ ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) ) )
56		sseq1	⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ⊆ dom 𝐺 ↔ suc 𝑦 ⊆ dom 𝐺 ) )
57		eleq2	⊢ ( 𝑥 = suc 𝑦 → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ↔ ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 ) )
58	56 57	anbi12d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) ↔ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 ) ) )
59		fveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ suc 𝑦 ) )
60	59	sseq2d	⊢ ( 𝑥 = suc 𝑦 → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ↔ ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) )
61	58 60	imbi12d	⊢ ( 𝑥 = suc 𝑦 → ( ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ) ↔ ( ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) )
62		noel	⊢ ¬ ( ◡ 𝐺 ‘ 𝐶 ) ∈ ∅
63	62	pm2.21i	⊢ ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ ∅ → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ ∅ ) )
64	63	adantl	⊢ ( ( ∅ ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ ∅ ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ ∅ ) )
65	64	a1i	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( ∅ ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ ∅ ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ ∅ ) ) )
66		fvex	⊢ ( ◡ 𝐺 ‘ 𝐶 ) ∈ V
67	66	elsuc	⊢ ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 ↔ ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ∨ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) )
68		sssucid	⊢ 𝑦 ⊆ suc 𝑦
69		sstr	⊢ ( ( 𝑦 ⊆ suc 𝑦 ∧ suc 𝑦 ⊆ dom 𝐺 ) → 𝑦 ⊆ dom 𝐺 )
70	68 69	mpan	⊢ ( suc 𝑦 ⊆ dom 𝐺 → 𝑦 ⊆ dom 𝐺 )
71	70	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) ) → 𝑦 ⊆ dom 𝐺 )
72		simprr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) ) → ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 )
73		pm2.27	⊢ ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) )
74	71 72 73	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) ) → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) )
75	6	cantnfvalf	⊢ 𝐻 : ω ⟶ On
76	75	ffvelcdmi	⊢ ( 𝑦 ∈ ω → ( 𝐻 ‘ 𝑦 ) ∈ On )
77	76	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐻 ‘ 𝑦 ) ∈ On )
78	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → 𝐴 ∈ On )
79	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → 𝐵 ∈ On )
80		suppssdm	⊢ ( 𝐹 supp ∅ ) ⊆ dom 𝐹
81	80 24	fssdm	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐵 )
82	81	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐹 supp ∅ ) ⊆ 𝐵 )
83		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → suc 𝑦 ⊆ dom 𝐺 )
84		sucidg	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ suc 𝑦 )
85	84	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → 𝑦 ∈ suc 𝑦 )
86	83 85	sseldd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → 𝑦 ∈ dom 𝐺 )
87	4	oif	⊢ 𝐺 : dom 𝐺 ⟶ ( 𝐹 supp ∅ )
88	87	ffvelcdmi	⊢ ( 𝑦 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
89	86 88	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
90	82 89	sseldd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐵 )
91		onelon	⊢ ( ( 𝐵 ∈ On ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝐺 ‘ 𝑦 ) ∈ On )
92	79 90 91	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐺 ‘ 𝑦 ) ∈ On )
93		oecl	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐺 ‘ 𝑦 ) ∈ On ) → ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ∈ On )
94	78 92 93	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ∈ On )
95	24	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → 𝐹 : 𝐵 ⟶ 𝐴 )
96	95 90	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ 𝐴 )
97		onelon	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ On )
98	78 96 97	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ On )
99		omcl	⊢ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ∈ On ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ On ) → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ On )
100	94 98 99	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ On )
101		oaword2	⊢ ( ( ( 𝐻 ‘ 𝑦 ) ∈ On ∧ ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ On ) → ( 𝐻 ‘ 𝑦 ) ⊆ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
102	77 100 101	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐻 ‘ 𝑦 ) ⊆ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
103	1 2 3 4 5 6	cantnfsuc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( 𝐻 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
104	103	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐻 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
105	102 104	sseqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( 𝐻 ‘ 𝑦 ) ⊆ ( 𝐻 ‘ suc 𝑦 ) )
106		sstr	⊢ ( ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ∧ ( 𝐻 ‘ 𝑦 ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) )
107	106	expcom	⊢ ( ( 𝐻 ‘ 𝑦 ) ⊆ ( 𝐻 ‘ suc 𝑦 ) → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) )
108	105 107	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) )
109	108	adantrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) ) → ( ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) )
110	74 109	syld	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) ) → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) )
111	110	expr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) )
112		simprr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 )
113	112	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐶 ) ) = ( 𝐺 ‘ 𝑦 ) )
114		f1ocnvfv2	⊢ ( ( 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) ∧ 𝐶 ∈ ( 𝐹 supp ∅ ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐶 ) ) = 𝐶 )
115	17 32 114	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐶 ) ) = 𝐶 )
116	115	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐶 ) ) = 𝐶 )
117	113 116	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( 𝐺 ‘ 𝑦 ) = 𝐶 )
118	117	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) = ( 𝐴 ↑o 𝐶 ) )
119	117	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) = ( 𝐹 ‘ 𝐶 ) )
120	118 119	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) )
121		oaword1	⊢ ( ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ On ∧ ( 𝐻 ‘ 𝑦 ) ∈ On ) → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ⊆ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
122	100 77 121	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ⊆ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
123	122	adantrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ⊆ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
124	120 123	eqsstrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
125	103	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( 𝐻 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
126	124 125	sseqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) )
127	126	expr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) )
128	127	a1dd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) )
129	111 128	jaod	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ∨ ( ◡ 𝐺 ‘ 𝐶 ) = 𝑦 ) → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) )
130	67 129	biimtrid	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) ∧ suc 𝑦 ⊆ dom 𝐺 ) → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) )
131	130	expimpd	⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) → ( ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 ) → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) )
132	131	com23	⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) ∧ 𝑦 ∈ ω ) → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) )
133	132	expcom	⊢ ( 𝑦 ∈ ω → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( ( 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑦 ) ) → ( ( suc 𝑦 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ suc 𝑦 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ suc 𝑦 ) ) ) ) )
134	49 55 61 65 133	finds2	⊢ ( 𝑥 ∈ ω → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( 𝑥 ⊆ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝐶 ) ∈ 𝑥 ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ 𝑥 ) ) ) )
135	43 134	vtoclga	⊢ ( dom 𝐺 ∈ ω → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ dom 𝐺 → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ dom 𝐺 ) ) ) )
136	35 135	mpcom	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( ◡ 𝐺 ‘ 𝐶 ) ∈ dom 𝐺 → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ dom 𝐺 ) ) )
137	33 136	mpd	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( 𝐻 ‘ dom 𝐺 ) )
138	1 2 3 4 5 6	cantnfval	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )
139	138	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )
140	137 139	sseqtrrd	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) ≠ ∅ ) → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) )
141		onelon	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ On )
142	3 7 141	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ On )
143		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐶 ) ∈ On )
144	2 142 143	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↑o 𝐶 ) ∈ On )
145		om0	⊢ ( ( 𝐴 ↑o 𝐶 ) ∈ On → ( ( 𝐴 ↑o 𝐶 ) ·o ∅ ) = ∅ )
146	144 145	syl	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐶 ) ·o ∅ ) = ∅ )
147		0ss	⊢ ∅ ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 )
148	146 147	eqsstrdi	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐶 ) ·o ∅ ) ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) )
149	9 140 148	pm2.61ne	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐶 ) ·o ( 𝐹 ‘ 𝐶 ) ) ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) )