Theorem cnfcomlem 9671

Description: Lemma for cnfcom 9672. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.)

Hypotheses

Ref	Expression
cnfcom.s	⊢ 𝑆 = dom (ω CNF 𝐴)
cnfcom.a	⊢ (𝜑 → 𝐴 ∈ On)
cnfcom.b	⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))
cnfcom.f	⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
cnfcom.g	⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
cnfcom.h	⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
cnfcom.t	⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
cnfcom.m	⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))
cnfcom.k	⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
cnfcom.1	⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
cnfcom.2	⊢ (𝜑 → 𝑂 ∈ (ω ↑o (𝐺‘𝐼)))
cnfcom.3	⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)

Assertion

Ref	Expression
cnfcomlem	⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))

Distinct variable groups:   𝑥,𝑘,𝑧,𝐴   𝑘,𝐼,𝑥,𝑧   𝑥,𝑀   𝑓,𝑘,𝑥,𝑧,𝐹   𝑧,𝑇   𝑓,𝐺,𝑘,𝑥,𝑧   𝑓,𝐻,𝑥   𝑆,𝑘,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑧, 𝑓, 𝑘)   𝐴(𝑓)   𝐵(𝑥, 𝑧, 𝑓, 𝑘)   𝑆(𝑥, 𝑓)   𝑇(𝑥, 𝑓, 𝑘)   𝐻(𝑧, 𝑘)   𝐼(𝑓)   𝐾(𝑥, 𝑧, 𝑓, 𝑘)   𝑀(𝑧, 𝑓, 𝑘)   𝑂(𝑥, 𝑧, 𝑓, 𝑘)

Proof of Theorem cnfcomlem

Dummy variables 𝑢 𝑣 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		omelon 9618	. . . . . . 7 ⊢ ω ∈ On
2		cnfcom.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ On)
3		suppssdm 8175	. . . . . . . . . 10 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 = dom (ω CNF 𝐴)
6	1	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ω ∈ On)
7	5, 6, 2	cantnff1o 9668	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
8		f1ocnv 6837	. . . . . . . . . . . . . . 15 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
9		f1of 6824	. . . . . . . . . . . . . . 15 ⊢ (◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
10	7, 8, 9	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11		cnfcom.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))
12	10, 11	ffvelcdmd 7084	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
13	4, 12	eqeltrid 2869	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
14	5, 6, 2	cantnfs 9638	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
15	13, 14	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
16	15	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
17	3, 16	fssdm 6729	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18		cnfcom.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
19		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
20	19	oif 9495	. . . . . . . . . . 11 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21	20	ffvelcdmi 7082	. . . . . . . . . 10 ⊢ (𝐼 ∈ dom 𝐺 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
22	18, 21	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
23	17, 22	sseldd 3939	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐴)
24		onelon 6389	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐺‘𝐼) ∈ 𝐴) → (𝐺‘𝐼) ∈ On)
25	2, 23, 24	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐼) ∈ On)
26		oecl 8524	. . . . . . 7 ⊢ ((ω ∈ On ∧ (𝐺‘𝐼) ∈ On) → (ω ↑o (𝐺‘𝐼)) ∈ On)
27	1, 25, 26	sylancr 599	. . . . . 6 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ∈ On)
28	16, 23	ffvelcdmd 7084	. . . . . . 7 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ ω)
29		nnon 7870	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ ω → (𝐹‘(𝐺‘𝐼)) ∈ On)
30	28, 29	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ On)
31		omcl 8523	. . . . . 6 ⊢ (((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
32	27, 30, 31	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
33	5, 6, 2, 19, 13	cantnfcl 9639	. . . . . . . 8 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
34	33	simprd 501	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 ∈ ω)
35		elnn 7875	. . . . . . 7 ⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
36	18, 34, 35	syl2anc 596	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ω)
37		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
38	37	cantnfvalf 9637	. . . . . . 7 ⊢ 𝐻:ω⟶On
39	38	ffvelcdmi 7082	. . . . . 6 ⊢ (𝐼 ∈ ω → (𝐻‘𝐼) ∈ On)
40	36, 39	syl 18	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐼) ∈ On)
41		eqid 2765	. . . . . 6 ⊢ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
42	41	oacomf1o 8552	. . . . 5 ⊢ ((((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On ∧ (𝐻‘𝐼) ∈ On) → ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
43	32, 40, 42	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
44		cnfcom.t	. . . . . . . 8 ⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
45	44	seqomsuc 8446	. . . . . . 7 ⊢ (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
46	36, 45	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
47		nfcv 2927	. . . . . . . . 9 ⊢ Ⅎ𝑢𝐾
48		nfcv 2927	. . . . . . . . 9 ⊢ Ⅎ𝑣𝐾
49		nfcv 2927	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
50		nfcv 2927	. . . . . . . . 9 ⊢ Ⅎ𝑓((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
51		cnfcom.k	. . . . . . . . . 10 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52		oveq2 7424	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
53	52	cbvmptv 5217	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦))
54		cnfcom.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))
55		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑘 = 𝑢)
56	55	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐺‘𝑘) = (𝐺‘𝑢))
57	56	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (ω ↑o (𝐺‘𝑘)) = (ω ↑o (𝐺‘𝑢)))
58	56	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑢)))
59	57, 58	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
60	54, 59	eqtrid 2812	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
61		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑓 = 𝑣)
62	61	dmeqd 5897	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
63	62	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
64	60, 63	mpteq12dv 5200	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
65	53, 64	eqtrid 2812	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66		oveq2 7424	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
67	66	cbvmptv 5217	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
68	60	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))
69	62, 68	mpteq12dv 5200	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
70	67, 69	eqtrid 2812	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
71	70	cnveqd 5863	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
72	65, 71	uneq12d 4123	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
73	51, 72	eqtrid 2812	. . . . . . . . 9 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
74	47, 48, 49, 50, 73	cbvmpo 7510	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
75	74	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))))
76		simprl 783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → 𝑢 = 𝐼)
77	76	fveq2d 6889	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐺‘𝑢) = (𝐺‘𝐼))
78	77	oveq2d 7432	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (ω ↑o (𝐺‘𝑢)) = (ω ↑o (𝐺‘𝐼)))
79	77	fveq2d 6889	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝐼)))
80	78, 79	oveq12d 7434	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
81		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → 𝑣 = (𝑇‘𝐼))
82	81	dmeqd 5897	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → dom 𝑣 = dom (𝑇‘𝐼))
83		cnfcom.3	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)
84		f1odm 6828	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
85	83, 84	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
86	82, 85	sylan9eqr 2822	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → dom 𝑣 = (𝐻‘𝐼))
87	86	oveq1d 7431	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻‘𝐼) +o 𝑦))
88	80, 87	mpteq12dv 5200	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)))
89	80	oveq1d 7431	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))
90	86, 89	mpteq12dv 5200	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
91	90	cnveqd 5863	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
92	88, 91	uneq12d 4123	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
93	18	elexd 3480	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
94		fvexd 6900	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝐼) ∈ V)
95		ovex 7449	. . . . . . . . . 10 ⊢ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ V
96	95	mptex 7225	. . . . . . . . 9 ⊢ (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∈ V
97		fvex 6898	. . . . . . . . . . 11 ⊢ (𝐻‘𝐼) ∈ V
98	97	mptex 7225	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
99	98	cnvex 7924	. . . . . . . . 9 ⊢ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
100	96, 99	unex 7748	. . . . . . . 8 ⊢ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))) ∈ V
101	100	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))) ∈ V)
102	75, 92, 93, 94, 101	ovmpod 7568	. . . . . 6 ⊢ (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
103	46, 102	eqtrd 2800	. . . . 5 ⊢ (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
104	103	f1oeq1d 6819	. . . 4 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))))
105	43, 104	mpbird 260	. . 3 ⊢ (𝜑 → (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
106	1	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → ω ∈ On)
107		simpl 488	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐴 ∈ On)
108		simpr 490	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐹 ∈ 𝑆)
109	54	oveq1i 7426	. . . . . . . . . 10 ⊢ (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)
110	109	a1i 11	. . . . . . . . 9 ⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
111	110	mpoeq3ia 7494	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
112		eqid 2765	. . . . . . . 8 ⊢ ∅ = ∅
113		seqomeq12 8443	. . . . . . . 8 ⊢ (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ∧ ∅ = ∅) → seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅))
114	111, 112, 113	mp2an 705	. . . . . . 7 ⊢ seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
115	37, 114	eqtri 2788	. . . . . 6 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
116	5, 106, 107, 19, 108, 115	cantnfsuc 9642	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
117	2, 13, 36, 116	syl21anc 851	. . . 4 ⊢ (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
118	117	f1oeq2d 6820	. . 3 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))))
119	105, 118	mpbird 260	. 2 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
120		sssucid 6447	. . . . . 6 ⊢ dom 𝐺 ⊆ suc dom 𝐺
121	120, 18	sselid 3936	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ suc dom 𝐺)
122		epelg 5564	. . . . . . . . . . 11 ⊢ (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
123	18, 122	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
124	123	biimpar 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 E 𝐼)
125		ovexd 7451	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
126	33	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → E We (𝐹 supp ∅))
127	19	oiiso 9502	. . . . . . . . . . . 12 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
128	125, 126, 127	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
129	128	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
130	19	oicl 9494	. . . . . . . . . . . 12 ⊢ Ord dom 𝐺
131		ordelss 6380	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
132	130, 18, 131	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ⊆ dom 𝐺)
133	132	sselda 3938	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ dom 𝐺)
134	18	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ dom 𝐺)
135		isorel 7330	. . . . . . . . . 10 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ 𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
136	129, 133, 134, 135	syl12anc 850	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
137	124, 136	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) E (𝐺‘𝐼))
138		fvex 6898	. . . . . . . . 9 ⊢ (𝐺‘𝐼) ∈ V
139	138	epeli 5565	. . . . . . . 8 ⊢ ((𝐺‘𝑦) E (𝐺‘𝐼) ↔ (𝐺‘𝑦) ∈ (𝐺‘𝐼))
140	137, 139	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ (𝐺‘𝐼))
141	140	ralrimiva 3159	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))
142		ffun 6712	. . . . . . . 8 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
143	20, 142	ax-mp 5	. . . . . . 7 ⊢ Fun 𝐺
144		funimass4 6949	. . . . . . 7 ⊢ ((Fun 𝐺 ∧ 𝐼 ⊆ dom 𝐺) → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
145	143, 132, 144	sylancr 599	. . . . . 6 ⊢ (𝜑 → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
146	141, 145	mpbird 260	. . . . 5 ⊢ (𝜑 → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
147	1	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ω ∈ On)
148		simpll 779	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐴 ∈ On)
149		simplr 781	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐹 ∈ 𝑆)
150		peano1 7887	. . . . . . 7 ⊢ ∅ ∈ ω
151	150	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ∅ ∈ ω)
152		simpr1 1213	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐼 ∈ suc dom 𝐺)
153		simpr2 1214	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺‘𝐼) ∈ On)
154		simpr3 1215	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
155	5, 147, 148, 19, 149, 115, 151, 152, 153, 154	cantnflt 9644	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
156	2, 13, 121, 25, 146, 155	syl23anc 1404	. . . 4 ⊢ (𝜑 → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
157	16	ffnd 6710	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
158		0ex 5272	. . . . . . . . . 10 ⊢ ∅ ∈ V
159	158	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ V)
160		elsuppfn 8168	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
161	157, 2, 159, 160	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
162		simpr 490	. . . . . . . 8 ⊢ (((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
163	161, 162	biimtrdi 256	. . . . . . 7 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅))
164	22, 163	mpd 16	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
165		on0eln0 6422	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
166	30, 165	syl 18	. . . . . 6 ⊢ (𝜑 → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
167	164, 166	mpbird 260	. . . . 5 ⊢ (𝜑 → ∅ ∈ (𝐹‘(𝐺‘𝐼)))
168		omword1 8560	. . . . 5 ⊢ ((((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺‘𝐼))) → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
169	27, 30, 167, 168	syl21anc 851	. . . 4 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
170		oaabs2 8637	. . . 4 ⊢ ((((𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)) ∧ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On) ∧ (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) → ((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
171	156, 32, 169, 170	syl21anc 851	. . 3 ⊢ (𝜑 → ((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
172	171	f1oeq3d 6821	. 2 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
173	119, 172	mpbid 235	1 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  Vcvv 3457   ∪ cun 3904   ⊆ wss 3906  ∅c0 4286   class class class wbr 5111   ↦ cmpt 5194   E cep 5562   We wwe 5615  ^◡ccnv 5662  dom cdm 5663   “ cima 5666  Ord word 6363  Oncon0 6364  suc csuc 6366  Fun wfun 6534   Fn wfn 6535  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540   Isom wiso 6541  (class class class)co 7416   ∈ cmpo 7418  ωcom 7864   supp csupp 8158  seq_ωcseqom 8436   +_o coa 8452   ·_o comu 8453   ↑_o coe 8454   finSupp cfsupp 9324  OrdIsocoi 9474   CNF ccnf 9633

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-inf2 9613

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-1st 7988  df-2nd 7989  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-seqom 8437  df-1o 8455  df-2o 8456  df-oadd 8459  df-omul 8460  df-oexp 8461  df-er 8696  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9325  df-oi 9475  df-cnf 9634

This theorem is used by:  cnfcom  9672