Theorem cnfcomlem 8479

Description: Lemma for cnfcom 8480. (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	⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴))
cnfcom.f	⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
cnfcom.g	⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
cnfcom.h	⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅)
cnfcom.t	⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
cnfcom.m	⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘)))
cnfcom.k	⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)))
cnfcom.1	⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
cnfcom.2	⊢ (𝜑 → 𝑂 ∈ (ω ↑𝑜 (𝐺‘𝐼)))
cnfcom.3	⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)

Assertion

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

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 8426	. . . . . . 7 ⊢ ω ∈ On
2		cnfcom.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ On)
3		suppssdm 7195	. . . . . . . . . 10 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = dom (ω CNF 𝐴)
6	1	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ω ∈ On)
7	5, 6, 2	cantnff1o 8476	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴))
8		f1ocnv 6062	. . . . . . . . . . . . . . . 16 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆)
9		f1of 6050	. . . . . . . . . . . . . . . 16 ⊢ (◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆)
10	7, 8, 9	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆)
11		cnfcom.b	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴))
12	10, 11	ffvelrnd 6268	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
13	4, 12	syl5eqel 2692	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
14	5, 6, 2	cantnfs 8446	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
15	13, 14	mpbid 221	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
16	15	simpld 474	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
17		fdm 5964	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶ω → dom 𝐹 = 𝐴)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝐹 = 𝐴)
19	3, 18	syl5sseq 3616	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
20		cnfcom.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
21		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
22	21	oif 8318	. . . . . . . . . . 11 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
23	22	ffvelrni 6266	. . . . . . . . . 10 ⊢ (𝐼 ∈ dom 𝐺 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
24	20, 23	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
25	19, 24	sseldd 3569	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐴)
26		onelon 5665	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐺‘𝐼) ∈ 𝐴) → (𝐺‘𝐼) ∈ On)
27	2, 25, 26	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐼) ∈ On)
28		oecl 7504	. . . . . . 7 ⊢ ((ω ∈ On ∧ (𝐺‘𝐼) ∈ On) → (ω ↑𝑜 (𝐺‘𝐼)) ∈ On)
29	1, 27, 28	sylancr 694	. . . . . 6 ⊢ (𝜑 → (ω ↑𝑜 (𝐺‘𝐼)) ∈ On)
30	16, 25	ffvelrnd 6268	. . . . . . 7 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ ω)
31		nnon 6963	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ ω → (𝐹‘(𝐺‘𝐼)) ∈ On)
32	30, 31	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ On)
33		omcl 7503	. . . . . 6 ⊢ (((ω ↑𝑜 (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) → ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On)
34	29, 32, 33	syl2anc 691	. . . . 5 ⊢ (𝜑 → ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On)
35	5, 6, 2, 21, 13	cantnfcl 8447	. . . . . . . 8 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
36	35	simprd 478	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 ∈ ω)
37		elnn 6967	. . . . . . 7 ⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
38	20, 36, 37	syl2anc 691	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ω)
39		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅)
40	39	cantnfvalf 8445	. . . . . . 7 ⊢ 𝐻:ω⟶On
41	40	ffvelrni 6266	. . . . . 6 ⊢ (𝐼 ∈ ω → (𝐻‘𝐼) ∈ On)
42	38, 41	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐼) ∈ On)
43		eqid 2610	. . . . . 6 ⊢ ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) = ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)))
44	43	oacomf1o 7532	. . . . 5 ⊢ ((((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On ∧ (𝐻‘𝐼) ∈ On) → ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))
45	34, 42, 44	syl2anc 691	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))
46		cnfcom.t	. . . . . . . 8 ⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
47	46	seqomsuc 7439	. . . . . . 7 ⊢ (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
48	38, 47	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
49		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑢𝐾
50		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑣𝐾
51		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))
52		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑓((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))
53		cnfcom.k	. . . . . . . . . 10 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)))
54		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (dom 𝑓 +𝑜 𝑥) = (dom 𝑓 +𝑜 𝑦))
55	54	cbvmptv 4678	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) = (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑦))
56		cnfcom.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘)))
57		simpl 472	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑘 = 𝑢)
58	57	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐺‘𝑘) = (𝐺‘𝑢))
59	58	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (ω ↑𝑜 (𝐺‘𝑘)) = (ω ↑𝑜 (𝐺‘𝑢)))
60	58	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑢)))
61	59, 60	oveq12d 6567	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) = ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))))
62	56, 61	syl5eq 2656	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑀 = ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))))
63		simpr 476	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑓 = 𝑣)
64	63	dmeqd 5248	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
65	64	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (dom 𝑓 +𝑜 𝑦) = (dom 𝑣 +𝑜 𝑦))
66	62, 65	mpteq12dv 4663	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑦)) = (𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)))
67	55, 66	syl5eq 2656	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) = (𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)))
68		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑀 +𝑜 𝑥) = (𝑀 +𝑜 𝑦))
69	68	cbvmptv 4678	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑦))
70	62	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑀 +𝑜 𝑦) = (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))
71	64, 70	mpteq12dv 4663	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))
72	69, 71	syl5eq 2656	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))
73	72	cnveqd 5220	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)) = ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))
74	67, 73	uneq12d 3730	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) = ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))))
75	53, 74	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))))
76	49, 50, 51, 52, 75	cbvmpt2 6632	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))))
77	76	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))))
78		simprl 790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → 𝑢 = 𝐼)
79	78	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐺‘𝑢) = (𝐺‘𝐼))
80	79	oveq2d 6565	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (ω ↑𝑜 (𝐺‘𝑢)) = (ω ↑𝑜 (𝐺‘𝐼)))
81	79	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝐼)))
82	80, 81	oveq12d 6567	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) = ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))
83		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → 𝑣 = (𝑇‘𝐼))
84	83	dmeqd 5248	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → dom 𝑣 = dom (𝑇‘𝐼))
85		cnfcom.3	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)
86		f1odm 6054	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
87	85, 86	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
88	84, 87	sylan9eqr 2666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → dom 𝑣 = (𝐻‘𝐼))
89	88	oveq1d 6564	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (dom 𝑣 +𝑜 𝑦) = ((𝐻‘𝐼) +𝑜 𝑦))
90	82, 89	mpteq12dv 4663	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) = (𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)))
91	82	oveq1d 6564	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦) = (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))
92	88, 91	mpteq12dv 4663	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)) = (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)))
93	92	cnveqd 5220	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)) = ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)))
94	90, 93	uneq12d 3730	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))) = ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))))
95		elex 3185	. . . . . . . 8 ⊢ (𝐼 ∈ dom 𝐺 → 𝐼 ∈ V)
96	20, 95	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
97		fvex 6113	. . . . . . . 8 ⊢ (𝑇‘𝐼) ∈ V
98	97	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝐼) ∈ V)
99		ovex 6577	. . . . . . . . . 10 ⊢ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ V
100	99	mptex 6390	. . . . . . . . 9 ⊢ (𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∈ V
101		fvex 6113	. . . . . . . . . . 11 ⊢ (𝐻‘𝐼) ∈ V
102	101	mptex 6390	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)) ∈ V
103	102	cnvex 7006	. . . . . . . . 9 ⊢ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)) ∈ V
104	100, 103	unex 6854	. . . . . . . 8 ⊢ ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) ∈ V
105	104	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) ∈ V)
106	77, 94, 96, 98, 105	ovmpt2d 6686	. . . . . 6 ⊢ (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)) = ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))))
107	48, 106	eqtrd 2644	. . . . 5 ⊢ (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))))
108		f1oeq1 6040	. . . . 5 ⊢ ((𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) → ((𝑇‘suc 𝐼):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))))
109	107, 108	syl 17	. . . 4 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ ((𝑦 ∈ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))))
110	45, 109	mpbird 246	. . 3 ⊢ (𝜑 → (𝑇‘suc 𝐼):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))
111	1	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → ω ∈ On)
112		simpl 472	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐴 ∈ On)
113		simpr 476	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐹 ∈ 𝑆)
114	56	oveq1i 6559	. . . . . . . . . 10 ⊢ (𝑀 +𝑜 𝑧) = (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)
115	114	a1i 11	. . . . . . . . 9 ⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +𝑜 𝑧) = (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧))
116	115	mpt2eq3ia 6618	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧))
117		eqid 2610	. . . . . . . 8 ⊢ ∅ = ∅
118		seqomeq12 7436	. . . . . . . 8 ⊢ (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)) ∧ ∅ = ∅) → seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅))
119	116, 117, 118	mp2an 704	. . . . . . 7 ⊢ seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅)
120	39, 119	eqtri 2632	. . . . . 6 ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅)
121	5, 111, 112, 21, 113, 120	cantnfsuc 8450	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼)))
122	2, 13, 38, 121	syl21anc 1317	. . . 4 ⊢ (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼)))
123		f1oeq2 6041	. . . 4 ⊢ ((𝐻‘suc 𝐼) = (((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼)) → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))))
124	122, 123	syl 17	. . 3 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))))
125	110, 124	mpbird 246	. 2 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))
126		sssucid 5719	. . . . . 6 ⊢ dom 𝐺 ⊆ suc dom 𝐺
127	126, 20	sseldi 3566	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ suc dom 𝐺)
128		epelg 4950	. . . . . . . . . . 11 ⊢ (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
129	20, 128	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
130	129	biimpar 501	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 E 𝐼)
131	2, 19	ssexd 4733	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
132	35	simpld 474	. . . . . . . . . . . 12 ⊢ (𝜑 → E We (𝐹 supp ∅))
133	21	oiiso 8325	. . . . . . . . . . . 12 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
134	131, 132, 133	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
135	134	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
136	21	oicl 8317	. . . . . . . . . . . 12 ⊢ Ord dom 𝐺
137		ordelss 5656	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
138	136, 20, 137	sylancr 694	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ⊆ dom 𝐺)
139	138	sselda 3568	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ dom 𝐺)
140	20	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ dom 𝐺)
141		isorel 6476	. . . . . . . . . 10 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ 𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
142	135, 139, 140, 141	syl12anc 1316	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
143	130, 142	mpbid 221	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) E (𝐺‘𝐼))
144		fvex 6113	. . . . . . . . 9 ⊢ (𝐺‘𝐼) ∈ V
145	144	epelc 4951	. . . . . . . 8 ⊢ ((𝐺‘𝑦) E (𝐺‘𝐼) ↔ (𝐺‘𝑦) ∈ (𝐺‘𝐼))
146	143, 145	sylib 207	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ (𝐺‘𝐼))
147	146	ralrimiva 2949	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))
148		ffun 5961	. . . . . . . 8 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
149	22, 148	ax-mp 5	. . . . . . 7 ⊢ Fun 𝐺
150		funimass4 6157	. . . . . . 7 ⊢ ((Fun 𝐺 ∧ 𝐼 ⊆ dom 𝐺) → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
151	149, 138, 150	sylancr 694	. . . . . 6 ⊢ (𝜑 → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
152	147, 151	mpbird 246	. . . . 5 ⊢ (𝜑 → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
153	1	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ω ∈ On)
154		simpll 786	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐴 ∈ On)
155		simplr 788	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐹 ∈ 𝑆)
156		peano1 6977	. . . . . . 7 ⊢ ∅ ∈ ω
157	156	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ∅ ∈ ω)
158		simpr1 1060	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐼 ∈ suc dom 𝐺)
159		simpr2 1061	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺‘𝐼) ∈ On)
160		simpr3 1062	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
161	5, 153, 154, 21, 155, 120, 157, 158, 159, 160	cantnflt 8452	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐻‘𝐼) ∈ (ω ↑𝑜 (𝐺‘𝐼)))
162	2, 13, 127, 27, 152, 161	syl23anc 1325	. . . 4 ⊢ (𝜑 → (𝐻‘𝐼) ∈ (ω ↑𝑜 (𝐺‘𝐼)))
163		ffn 5958	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶ω → 𝐹 Fn 𝐴)
164	16, 163	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
165		0ex 4718	. . . . . . . . . 10 ⊢ ∅ ∈ V
166	165	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ V)
167		elsuppfn 7190	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
168	164, 2, 166, 167	syl3anc 1318	. . . . . . . 8 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
169		simpr 476	. . . . . . . 8 ⊢ (((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
170	168, 169	syl6bi 242	. . . . . . 7 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅))
171	24, 170	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
172		on0eln0 5697	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
173	32, 172	syl 17	. . . . . 6 ⊢ (𝜑 → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
174	171, 173	mpbird 246	. . . . 5 ⊢ (𝜑 → ∅ ∈ (𝐹‘(𝐺‘𝐼)))
175		omword1 7540	. . . . 5 ⊢ ((((ω ↑𝑜 (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺‘𝐼))) → (ω ↑𝑜 (𝐺‘𝐼)) ⊆ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))
176	29, 32, 174, 175	syl21anc 1317	. . . 4 ⊢ (𝜑 → (ω ↑𝑜 (𝐺‘𝐼)) ⊆ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))
177		oaabs2 7612	. . . 4 ⊢ ((((𝐻‘𝐼) ∈ (ω ↑𝑜 (𝐺‘𝐼)) ∧ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On) ∧ (ω ↑𝑜 (𝐺‘𝐼)) ⊆ ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) → ((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) = ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))
178	162, 34, 176, 177	syl21anc 1317	. . 3 ⊢ (𝜑 → ((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) = ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))
179		f1oeq3 6042	. . 3 ⊢ (((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) = ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))
180	178, 179	syl 17	. 2 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))
181	125, 180	mpbid 221	1 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   ↦ cmpt 4643   E cep 4947   We wwe 4996  ^◡ccnv 5037  dom cdm 5038   “ cima 5041  Ord word 5639  Oncon0 5640  suc csuc 5642  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805  (class class class)co 6549   ↦ cmpt2 6551  ωcom 6957   supp csupp 7182  seq_𝜔cseqom 7429   +_𝑜 coa 7444   ·_𝑜 comu 7445   ↑_𝑜 coe 7446   finSupp cfsupp 8158  OrdIsocoi 8297   CNF ccnf 8441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-seqom 7430  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-oexp 7453  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-cnf 8442

This theorem is referenced by:  cnfcom  8480