Theorem cnfcomlem 9635

Description: Lemma for cnfcom 9636. (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 9582	. . . . . . 7 ⊢ ω ∈ On
2		cnfcom.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ On)
3		suppssdm 8108	. . . . . . . . . 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 9632	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
8		f1ocnv 6796	. . . . . . . . . . . . . . 15 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
9		f1of 6784	. . . . . . . . . . . . . . 15 ⊢ (◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
10	7, 8, 9	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11		cnfcom.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))
12	10, 11	ffvelcdmd 7036	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
13	4, 12	eqeltrid 2842	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
14	5, 6, 2	cantnfs 9602	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
15	13, 14	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
16	15	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
17	3, 16	fssdm 6688	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18		cnfcom.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
19		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
20	19	oif 9466	. . . . . . . . . . 11 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21	20	ffvelcdmi 7034	. . . . . . . . . 10 ⊢ (𝐼 ∈ dom 𝐺 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
22	18, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
23	17, 22	sseldd 3945	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐴)
24		onelon 6342	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐺‘𝐼) ∈ 𝐴) → (𝐺‘𝐼) ∈ On)
25	2, 23, 24	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐼) ∈ On)
26		oecl 8483	. . . . . . 7 ⊢ ((ω ∈ On ∧ (𝐺‘𝐼) ∈ On) → (ω ↑o (𝐺‘𝐼)) ∈ On)
27	1, 25, 26	sylancr 587	. . . . . 6 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ∈ On)
28	16, 23	ffvelcdmd 7036	. . . . . . 7 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ ω)
29		nnon 7808	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ ω → (𝐹‘(𝐺‘𝐼)) ∈ On)
30	28, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ On)
31		omcl 8482	. . . . . 6 ⊢ (((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
32	27, 30, 31	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
33	5, 6, 2, 19, 13	cantnfcl 9603	. . . . . . . 8 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
34	33	simprd 496	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 ∈ ω)
35		elnn 7813	. . . . . . 7 ⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
36	18, 34, 35	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ω)
37		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
38	37	cantnfvalf 9601	. . . . . . 7 ⊢ 𝐻:ω⟶On
39	38	ffvelcdmi 7034	. . . . . 6 ⊢ (𝐼 ∈ ω → (𝐻‘𝐼) ∈ On)
40	36, 39	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐼) ∈ On)
41		eqid 2736	. . . . . 6 ⊢ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
42	41	oacomf1o 8512	. . . . 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 584	. . . 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 8403	. . . . . . 7 ⊢ (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
46	36, 45	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
47		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑢𝐾
48		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑣𝐾
49		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
50		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑓((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
51		cnfcom.k	. . . . . . . . . 10 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52		oveq2 7365	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
53	52	cbvmptv 5218	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦))
54		cnfcom.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))
55		simpl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑘 = 𝑢)
56	55	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐺‘𝑘) = (𝐺‘𝑢))
57	56	oveq2d 7373	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (ω ↑o (𝐺‘𝑘)) = (ω ↑o (𝐺‘𝑢)))
58	56	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑢)))
59	57, 58	oveq12d 7375	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
60	54, 59	eqtrid 2788	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
61		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑓 = 𝑣)
62	61	dmeqd 5861	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
63	62	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
64	60, 63	mpteq12dv 5196	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
65	53, 64	eqtrid 2788	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66		oveq2 7365	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
67	66	cbvmptv 5218	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
68	60	oveq1d 7372	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))
69	62, 68	mpteq12dv 5196	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
70	67, 69	eqtrid 2788	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
71	70	cnveqd 5831	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
72	65, 71	uneq12d 4124	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
73	51, 72	eqtrid 2788	. . . . . . . . 9 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
74	47, 48, 49, 50, 73	cbvmpo 7451	. . . . . . . 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 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → 𝑢 = 𝐼)
77	76	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐺‘𝑢) = (𝐺‘𝐼))
78	77	oveq2d 7373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (ω ↑o (𝐺‘𝑢)) = (ω ↑o (𝐺‘𝐼)))
79	77	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝐼)))
80	78, 79	oveq12d 7375	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
81		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → 𝑣 = (𝑇‘𝐼))
82	81	dmeqd 5861	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → dom 𝑣 = dom (𝑇‘𝐼))
83		cnfcom.3	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)
84		f1odm 6788	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
86	82, 85	sylan9eqr 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → dom 𝑣 = (𝐻‘𝐼))
87	86	oveq1d 7372	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻‘𝐼) +o 𝑦))
88	80, 87	mpteq12dv 5196	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)))
89	80	oveq1d 7372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))
90	86, 89	mpteq12dv 5196	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
91	90	cnveqd 5831	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
92	88, 91	uneq12d 4124	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
93	18	elexd 3465	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
94		fvexd 6857	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝐼) ∈ V)
95		ovex 7390	. . . . . . . . . 10 ⊢ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ V
96	95	mptex 7173	. . . . . . . . 9 ⊢ (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∈ V
97		fvex 6855	. . . . . . . . . . 11 ⊢ (𝐻‘𝐼) ∈ V
98	97	mptex 7173	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
99	98	cnvex 7862	. . . . . . . . 9 ⊢ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
100	96, 99	unex 7680	. . . . . . . 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 7507	. . . . . 6 ⊢ (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
103	46, 102	eqtrd 2776	. . . . 5 ⊢ (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
104	103	f1oeq1d 6779	. . . 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 256	. . 3 ⊢ (𝜑 → (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
106	1	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → ω ∈ On)
107		simpl 483	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐴 ∈ On)
108		simpr 485	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐹 ∈ 𝑆)
109	54	oveq1i 7367	. . . . . . . . . 10 ⊢ (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)
110	109	a1i 11	. . . . . . . . 9 ⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
111	110	mpoeq3ia 7435	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
112		eqid 2736	. . . . . . . 8 ⊢ ∅ = ∅
113		seqomeq12 8400	. . . . . . . 8 ⊢ (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ∧ ∅ = ∅) → seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅))
114	111, 112, 113	mp2an 690	. . . . . . 7 ⊢ seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
115	37, 114	eqtri 2764	. . . . . 6 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
116	5, 106, 107, 19, 108, 115	cantnfsuc 9606	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
117	2, 13, 36, 116	syl21anc 836	. . . 4 ⊢ (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
118	117	f1oeq2d 6780	. . 3 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))))
119	105, 118	mpbird 256	. 2 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
120		sssucid 6397	. . . . . 6 ⊢ dom 𝐺 ⊆ suc dom 𝐺
121	120, 18	sselid 3942	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ suc dom 𝐺)
122		epelg 5538	. . . . . . . . . . 11 ⊢ (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
123	18, 122	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
124	123	biimpar 478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 E 𝐼)
125		ovexd 7392	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
126	33	simpld 495	. . . . . . . . . . . 12 ⊢ (𝜑 → E We (𝐹 supp ∅))
127	19	oiiso 9473	. . . . . . . . . . . 12 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
128	125, 126, 127	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
129	128	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
130	19	oicl 9465	. . . . . . . . . . . 12 ⊢ Ord dom 𝐺
131		ordelss 6333	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
132	130, 18, 131	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ⊆ dom 𝐺)
133	132	sselda 3944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ dom 𝐺)
134	18	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ dom 𝐺)
135		isorel 7271	. . . . . . . . . 10 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ 𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
136	129, 133, 134, 135	syl12anc 835	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
137	124, 136	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) E (𝐺‘𝐼))
138		fvex 6855	. . . . . . . . 9 ⊢ (𝐺‘𝐼) ∈ V
139	138	epeli 5539	. . . . . . . 8 ⊢ ((𝐺‘𝑦) E (𝐺‘𝐼) ↔ (𝐺‘𝑦) ∈ (𝐺‘𝐼))
140	137, 139	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ (𝐺‘𝐼))
141	140	ralrimiva 3143	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))
142		ffun 6671	. . . . . . . 8 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
143	20, 142	ax-mp 5	. . . . . . 7 ⊢ Fun 𝐺
144		funimass4 6907	. . . . . . 7 ⊢ ((Fun 𝐺 ∧ 𝐼 ⊆ dom 𝐺) → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
145	143, 132, 144	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
146	141, 145	mpbird 256	. . . . 5 ⊢ (𝜑 → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
147	1	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ω ∈ On)
148		simpll 765	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐴 ∈ On)
149		simplr 767	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐹 ∈ 𝑆)
150		peano1 7825	. . . . . . 7 ⊢ ∅ ∈ ω
151	150	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ∅ ∈ ω)
152		simpr1 1194	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐼 ∈ suc dom 𝐺)
153		simpr2 1195	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺‘𝐼) ∈ On)
154		simpr3 1196	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
155	5, 147, 148, 19, 149, 115, 151, 152, 153, 154	cantnflt 9608	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
156	2, 13, 121, 25, 146, 155	syl23anc 1377	. . . 4 ⊢ (𝜑 → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
157	16	ffnd 6669	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
158		0ex 5264	. . . . . . . . . 10 ⊢ ∅ ∈ V
159	158	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ V)
160		elsuppfn 8102	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
161	157, 2, 159, 160	syl3anc 1371	. . . . . . . 8 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
162		simpr 485	. . . . . . . 8 ⊢ (((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
163	161, 162	syl6bi 252	. . . . . . 7 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅))
164	22, 163	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
165		on0eln0 6373	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
166	30, 165	syl 17	. . . . . 6 ⊢ (𝜑 → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
167	164, 166	mpbird 256	. . . . 5 ⊢ (𝜑 → ∅ ∈ (𝐹‘(𝐺‘𝐼)))
168		omword1 8520	. . . . 5 ⊢ ((((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺‘𝐼))) → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
169	27, 30, 167, 168	syl21anc 836	. . . 4 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
170		oaabs2 8595	. . . 4 ⊢ ((((𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)) ∧ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On) ∧ (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) → ((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
171	156, 32, 169, 170	syl21anc 836	. . 3 ⊢ (𝜑 → ((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
172	171	f1oeq3d 6781	. 2 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
173	119, 172	mpbid 231	1 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  Vcvv 3445   ∪ cun 3908   ⊆ wss 3910  ∅c0 4282   class class class wbr 5105   ↦ cmpt 5188   E cep 5536   We wwe 5587  ^◡ccnv 5632  dom cdm 5633   “ cima 5636  Ord word 6316  Oncon0 6317  suc csuc 6319  Fun wfun 6490   Fn wfn 6491  ⟶wf 6492  –1-1-onto→wf1o 6495  ‘cfv 6496   Isom wiso 6497  (class class class)co 7357   ∈ cmpo 7359  ωcom 7802   supp csupp 8092  seq_ωcseqom 8393   +_o coa 8409   ·_o comu 8410   ↑_o coe 8411   finSupp cfsupp 9305  OrdIsocoi 9445   CNF ccnf 9597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-seqom 8394  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-oexp 8418  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-oi 9446  df-cnf 9598

This theorem is referenced by:  cnfcom  9636