Theorem cnfcomlem 9693

Description: Lemma for cnfcom 9694. (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 9640	. . . . . . 7 ⊢ ω ∈ On
2		cnfcom.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ On)
3		suppssdm 8161	. . . . . . . . . 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 9690	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
8		f1ocnv 6845	. . . . . . . . . . . . . . 15 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
9		f1of 6833	. . . . . . . . . . . . . . 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 7087	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
13	4, 12	eqeltrid 2837	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
14	5, 6, 2	cantnfs 9660	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
15	13, 14	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
16	15	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
17	3, 16	fssdm 6737	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18		cnfcom.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
19		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
20	19	oif 9524	. . . . . . . . . . 11 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21	20	ffvelcdmi 7085	. . . . . . . . . 10 ⊢ (𝐼 ∈ dom 𝐺 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
22	18, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
23	17, 22	sseldd 3983	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐴)
24		onelon 6389	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐺‘𝐼) ∈ 𝐴) → (𝐺‘𝐼) ∈ On)
25	2, 23, 24	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐼) ∈ On)
26		oecl 8536	. . . . . . 7 ⊢ ((ω ∈ On ∧ (𝐺‘𝐼) ∈ On) → (ω ↑o (𝐺‘𝐼)) ∈ On)
27	1, 25, 26	sylancr 587	. . . . . 6 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ∈ On)
28	16, 23	ffvelcdmd 7087	. . . . . . 7 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ ω)
29		nnon 7860	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ ω → (𝐹‘(𝐺‘𝐼)) ∈ On)
30	28, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ On)
31		omcl 8535	. . . . . 6 ⊢ (((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
32	27, 30, 31	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
33	5, 6, 2, 19, 13	cantnfcl 9661	. . . . . . . 8 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
34	33	simprd 496	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 ∈ ω)
35		elnn 7865	. . . . . . 7 ⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
36	18, 34, 35	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ω)
37		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
38	37	cantnfvalf 9659	. . . . . . 7 ⊢ 𝐻:ω⟶On
39	38	ffvelcdmi 7085	. . . . . 6 ⊢ (𝐼 ∈ ω → (𝐻‘𝐼) ∈ On)
40	36, 39	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐼) ∈ On)
41		eqid 2732	. . . . . 6 ⊢ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
42	41	oacomf1o 8564	. . . . 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 8456	. . . . . . 7 ⊢ (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
46	36, 45	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
47		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑢𝐾
48		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑣𝐾
49		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
50		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑓((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
51		cnfcom.k	. . . . . . . . . 10 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52		oveq2 7416	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
53	52	cbvmptv 5261	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦))
54		cnfcom.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))
55		simpl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑘 = 𝑢)
56	55	fveq2d 6895	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐺‘𝑘) = (𝐺‘𝑢))
57	56	oveq2d 7424	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (ω ↑o (𝐺‘𝑘)) = (ω ↑o (𝐺‘𝑢)))
58	56	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑢)))
59	57, 58	oveq12d 7426	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
60	54, 59	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
61		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑓 = 𝑣)
62	61	dmeqd 5905	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
63	62	oveq1d 7423	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
64	60, 63	mpteq12dv 5239	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
65	53, 64	eqtrid 2784	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66		oveq2 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
67	66	cbvmptv 5261	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
68	60	oveq1d 7423	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))
69	62, 68	mpteq12dv 5239	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
70	67, 69	eqtrid 2784	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
71	70	cnveqd 5875	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
72	65, 71	uneq12d 4164	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
73	51, 72	eqtrid 2784	. . . . . . . . 9 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
74	47, 48, 49, 50, 73	cbvmpo 7502	. . . . . . . 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 6895	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐺‘𝑢) = (𝐺‘𝐼))
78	77	oveq2d 7424	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (ω ↑o (𝐺‘𝑢)) = (ω ↑o (𝐺‘𝐼)))
79	77	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝐼)))
80	78, 79	oveq12d 7426	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
81		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → 𝑣 = (𝑇‘𝐼))
82	81	dmeqd 5905	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → dom 𝑣 = dom (𝑇‘𝐼))
83		cnfcom.3	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)
84		f1odm 6837	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
86	82, 85	sylan9eqr 2794	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → dom 𝑣 = (𝐻‘𝐼))
87	86	oveq1d 7423	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻‘𝐼) +o 𝑦))
88	80, 87	mpteq12dv 5239	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)))
89	80	oveq1d 7423	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))
90	86, 89	mpteq12dv 5239	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
91	90	cnveqd 5875	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
92	88, 91	uneq12d 4164	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
93	18	elexd 3494	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
94		fvexd 6906	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝐼) ∈ V)
95		ovex 7441	. . . . . . . . . 10 ⊢ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ V
96	95	mptex 7224	. . . . . . . . 9 ⊢ (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∈ V
97		fvex 6904	. . . . . . . . . . 11 ⊢ (𝐻‘𝐼) ∈ V
98	97	mptex 7224	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
99	98	cnvex 7915	. . . . . . . . 9 ⊢ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
100	96, 99	unex 7732	. . . . . . . 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 7559	. . . . . 6 ⊢ (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
103	46, 102	eqtrd 2772	. . . . 5 ⊢ (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
104	103	f1oeq1d 6828	. . . 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 7418	. . . . . . . . . 10 ⊢ (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)
110	109	a1i 11	. . . . . . . . 9 ⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
111	110	mpoeq3ia 7486	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
112		eqid 2732	. . . . . . . 8 ⊢ ∅ = ∅
113		seqomeq12 8453	. . . . . . . 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 2760	. . . . . 6 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
116	5, 106, 107, 19, 108, 115	cantnfsuc 9664	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
117	2, 13, 36, 116	syl21anc 836	. . . 4 ⊢ (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
118	117	f1oeq2d 6829	. . 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 6444	. . . . . 6 ⊢ dom 𝐺 ⊆ suc dom 𝐺
121	120, 18	sselid 3980	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ suc dom 𝐺)
122		epelg 5581	. . . . . . . . . . 11 ⊢ (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
123	18, 122	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
124	123	biimpar 478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 E 𝐼)
125		ovexd 7443	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
126	33	simpld 495	. . . . . . . . . . . 12 ⊢ (𝜑 → E We (𝐹 supp ∅))
127	19	oiiso 9531	. . . . . . . . . . . 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 9523	. . . . . . . . . . . 12 ⊢ Ord dom 𝐺
131		ordelss 6380	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
132	130, 18, 131	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ⊆ dom 𝐺)
133	132	sselda 3982	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ dom 𝐺)
134	18	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ dom 𝐺)
135		isorel 7322	. . . . . . . . . 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 6904	. . . . . . . . 9 ⊢ (𝐺‘𝐼) ∈ V
139	138	epeli 5582	. . . . . . . 8 ⊢ ((𝐺‘𝑦) E (𝐺‘𝐼) ↔ (𝐺‘𝑦) ∈ (𝐺‘𝐼))
140	137, 139	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ (𝐺‘𝐼))
141	140	ralrimiva 3146	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))
142		ffun 6720	. . . . . . . 8 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
143	20, 142	ax-mp 5	. . . . . . 7 ⊢ Fun 𝐺
144		funimass4 6956	. . . . . . 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 7878	. . . . . . 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 9666	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
156	2, 13, 121, 25, 146, 155	syl23anc 1377	. . . 4 ⊢ (𝜑 → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
157	16	ffnd 6718	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
158		0ex 5307	. . . . . . . . . 10 ⊢ ∅ ∈ V
159	158	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ V)
160		elsuppfn 8155	. . . . . . . . 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 6420	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
166	30, 165	syl 17	. . . . . 6 ⊢ (𝜑 → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
167	164, 166	mpbird 256	. . . . 5 ⊢ (𝜑 → ∅ ∈ (𝐹‘(𝐺‘𝐼)))
168		omword1 8572	. . . . 5 ⊢ ((((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺‘𝐼))) → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
169	27, 30, 167, 168	syl21anc 836	. . . 4 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
170		oaabs2 8647	. . . 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 6830	. 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 2940  ∀wral 3061  Vcvv 3474   ∪ cun 3946   ⊆ wss 3948  ∅c0 4322   class class class wbr 5148   ↦ cmpt 5231   E cep 5579   We wwe 5630  ^◡ccnv 5675  dom cdm 5676   “ cima 5679  Ord word 6363  Oncon0 6364  suc csuc 6366  Fun wfun 6537   Fn wfn 6538  ⟶wf 6539  –1-1-onto→wf1o 6542  ‘cfv 6543   Isom wiso 6544  (class class class)co 7408   ∈ cmpo 7410  ωcom 7854   supp csupp 8145  seq_ωcseqom 8446   +_o coa 8462   ·_o comu 8463   ↑_o coe 8464   finSupp cfsupp 9360  OrdIsocoi 9503   CNF ccnf 9655

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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-inf2 9635

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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-supp 8146  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-seqom 8447  df-1o 8465  df-2o 8466  df-oadd 8469  df-omul 8470  df-oexp 8471  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-oi 9504  df-cnf 9656

This theorem is referenced by:  cnfcom  9694