This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) ‘ 𝐹 ) )