Theorem cnfcomlem 9735

Description: Lemma for cnfcom 9736. (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-1onto𝑂)

Assertion

Ref	Expression
cnfcomlem	⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)⟶1-1onto((ω ↑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 9682	. . . . . . 7 ⊢ ω ∈ On
2		cnfcom.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ On)
3		suppssdm 8230	. . . . . . . . . 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 9732	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ω CNF 𝐴):𝑆⟶1-1onto(ω ↑o 𝐴))
8		f1ocnv 6865	. . . . . . . . . . . . . . 15 ⊢ ((ω CNF 𝐴):𝑆⟶1-1onto(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶1-1onto𝑆)
9		f1of 6852	. . . . . . . . . . . . . . 15 ⊢ (◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶1-1onto𝑆 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
10	7, 8, 9	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11		cnfcom.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))
12	10, 11	ffvelcdmd 7115	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
13	4, 12	eqeltrid 2868	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
14	5, 6, 2	cantnfs 9702	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
15	13, 14	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
16	15	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
17	3, 16	fssdm 6757	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18		cnfcom.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
19		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
20	19	oif 9559	. . . . . . . . . . 11 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21	20	ffvelcdmi 7113	. . . . . . . . . 10 ⊢ (𝐼 ∈ dom 𝐺 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
22	18, 21	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
23	17, 22	sseldd 3914	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐴)
24		onelon 6411	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐺‘𝐼) ∈ 𝐴) → (𝐺‘𝐼) ∈ On)
25	2, 23, 24	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐼) ∈ On)
26		oecl 8581	. . . . . . 7 ⊢ ((ω ∈ On ∧ (𝐺‘𝐼) ∈ On) → (ω ↑o (𝐺‘𝐼)) ∈ On)
27	1, 25, 26	sylancr 599	. . . . . 6 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ∈ On)
28	16, 23	ffvelcdmd 7115	. . . . . . 7 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ ω)
29		nnon 7915	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ ω → (𝐹‘(𝐺‘𝐼)) ∈ On)
30	28, 29	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ On)
31		omcl 8580	. . . . . 6 ⊢ (((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
32	27, 30, 31	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
33	5, 6, 2, 19, 13	cantnfcl 9703	. . . . . . . 8 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
34	33	simprd 501	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 ∈ ω)
35		elnn 7920	. . . . . . 7 ⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
36	18, 34, 35	syl2anc 596	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ω)
37		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
38	37	cantnfvalf 9701	. . . . . . 7 ⊢ 𝐻:ω⟶On
39	38	ffvelcdmi 7113	. . . . . 6 ⊢ (𝐼 ∈ ω → (𝐻‘𝐼) ∈ On)
40	36, 39	syl 18	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐼) ∈ On)
41		eqid 2763	. . . . . 6 ⊢ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
42	41	oacomf1o 8609	. . . . 5 ⊢ ((((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On ∧ (𝐻‘𝐼) ∈ On) → ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
43	32, 40, 42	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
44		cnfcom.t	. . . . . . . 8 ⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
45	44	seqomsuc 8503	. . . . . . 7 ⊢ (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
46	36, 45	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
47		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑢𝐾
48		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑣𝐾
49		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
50		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑓((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
51		cnfcom.k	. . . . . . . . . 10 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52		oveq2 7457	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
53	52	cbvmptv 5213	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦))
54		cnfcom.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))
55		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑘 = 𝑢)
56	55	fveq2d 6918	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐺‘𝑘) = (𝐺‘𝑢))
57	56	oveq2d 7465	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (ω ↑o (𝐺‘𝑘)) = (ω ↑o (𝐺‘𝑢)))
58	56	fveq2d 6918	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑢)))
59	57, 58	oveq12d 7467	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
60	54, 59	eqtrid 2810	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
61		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑓 = 𝑣)
62	61	dmeqd 5897	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
63	62	oveq1d 7464	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
64	60, 63	mpteq12dv 5196	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
65	53, 64	eqtrid 2810	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66		oveq2 7457	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
67	66	cbvmptv 5213	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
68	60	oveq1d 7464	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))
69	62, 68	mpteq12dv 5196	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
70	67, 69	eqtrid 2810	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
71	70	cnveqd 5863	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
72	65, 71	uneq12d 4171	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
73	51, 72	eqtrid 2810	. . . . . . . . 9 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
74	47, 48, 49, 50, 73	cbvmpo 7543	. . . . . . . 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 6918	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐺‘𝑢) = (𝐺‘𝐼))
78	77	oveq2d 7465	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (ω ↑o (𝐺‘𝑢)) = (ω ↑o (𝐺‘𝐼)))
79	77	fveq2d 6918	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝐼)))
80	78, 79	oveq12d 7467	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
81		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → 𝑣 = (𝑇‘𝐼))
82	81	dmeqd 5897	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → dom 𝑣 = dom (𝑇‘𝐼))
83		cnfcom.3	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)⟶1-1onto𝑂)
84		f1odm 6856	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐼):(𝐻‘𝐼)⟶1-1onto𝑂 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
85	83, 84	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
86	82, 85	sylan9eqr 2820	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → dom 𝑣 = (𝐻‘𝐼))
87	86	oveq1d 7464	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻‘𝐼) +o 𝑦))
88	80, 87	mpteq12dv 5196	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)))
89	80	oveq1d 7464	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))
90	86, 89	mpteq12dv 5196	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
91	90	cnveqd 5863	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
92	88, 91	uneq12d 4171	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
93	18	elexd 3477	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
94		fvexd 6929	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝐼) ∈ V)
95		ovex 7482	. . . . . . . . . 10 ⊢ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ V
96	95	mptex 7258	. . . . . . . . 9 ⊢ (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∈ V
97		fvex 6927	. . . . . . . . . . 11 ⊢ (𝐻‘𝐼) ∈ V
98	97	mptex 7258	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
99	98	cnvex 7969	. . . . . . . . 9 ⊢ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
100	96, 99	unex 7791	. . . . . . . 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 7602	. . . . . 6 ⊢ (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
103	46, 102	eqtrd 2798	. . . . 5 ⊢ (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
104	103	f1oeq1d 6847	. . . 4 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))))
105	43, 104	mpbird 260	. . 3 ⊢ (𝜑 → (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
106	1	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → ω ∈ On)
107		simpl 488	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐴 ∈ On)
108		simpr 490	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐹 ∈ 𝑆)
109	54	oveq1i 7459	. . . . . . . . . 10 ⊢ (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)
110	109	a1i 11	. . . . . . . . 9 ⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
111	110	mpoeq3ia 7527	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
112		eqid 2763	. . . . . . . 8 ⊢ ∅ = ∅
113		seqomeq12 8500	. . . . . . . 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 2786	. . . . . 6 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
116	5, 106, 107, 19, 108, 115	cantnfsuc 9706	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
117	2, 13, 36, 116	syl21anc 851	. . . 4 ⊢ (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
118	117	f1oeq2d 6848	. . 3 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))))
119	105, 118	mpbird 260	. 2 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
120		sssucid 6469	. . . . . 6 ⊢ dom 𝐺 ⊆ suc dom 𝐺
121	120, 18	sselid 3911	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ suc dom 𝐺)
122		epelg 5557	. . . . . . . . . . 11 ⊢ (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
123	18, 122	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
124	123	biimpar 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 E 𝐼)
125		ovexd 7484	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
126	33	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → E We (𝐹 supp ∅))
127	19	oiiso 9566	. . . . . . . . . . . 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 9558	. . . . . . . . . . . 12 ⊢ Ord dom 𝐺
131		ordelss 6402	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
132	130, 18, 131	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ⊆ dom 𝐺)
133	132	sselda 3913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ dom 𝐺)
134	18	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ dom 𝐺)
135		isorel 7363	. . . . . . . . . 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 6927	. . . . . . . . 9 ⊢ (𝐺‘𝐼) ∈ V
139	138	epeli 5558	. . . . . . . 8 ⊢ ((𝐺‘𝑦) E (𝐺‘𝐼) ↔ (𝐺‘𝑦) ∈ (𝐺‘𝐼))
140	137, 139	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ (𝐺‘𝐼))
141	140	ralrimiva 3158	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))
142		ffun 6740	. . . . . . . 8 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
143	20, 142	ax-mp 5	. . . . . . 7 ⊢ Fun 𝐺
144		funimass4 6978	. . . . . . 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 7932	. . . . . . 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 9708	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
156	2, 13, 121, 25, 146, 155	syl23anc 1405	. . . 4 ⊢ (𝜑 → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
157	16	ffnd 6738	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
158		0ex 5265	. . . . . . . . . 10 ⊢ ∅ ∈ V
159	158	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ V)
160		elsuppfn 8223	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
161	157, 2, 159, 160	syl3anc 1399	. . . . . . . 8 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
162		simpr 490	. . . . . . . 8 ⊢ (((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
163	161, 162	biimtrdi 256	. . . . . . 7 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅))
164	22, 163	mpd 16	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
165		on0eln0 6444	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
166	30, 165	syl 18	. . . . . 6 ⊢ (𝜑 → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
167	164, 166	mpbird 260	. . . . 5 ⊢ (𝜑 → ∅ ∈ (𝐹‘(𝐺‘𝐼)))
168		omword1 8617	. . . . 5 ⊢ ((((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺‘𝐼))) → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
169	27, 30, 167, 168	syl21anc 851	. . . 4 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
170		oaabs2 8694	. . . 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 6849	. 2 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)⟶1-1onto((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)⟶1-1onto((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
173	119, 172	mpbid 235	1 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)⟶1-1onto((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  Vcvv 3454   ⊆ wss 3900   ∪ cun 4152  ∅c0 4281   class class class wbr 5106   ↦ cmpt 5190   E cep 5555   We wwe 5608  ^◡ccnv 5655  dom cdm 5656   “ cima 5659  Ord word 6385  Oncon0 6386  suc csuc 6388  Fun wfun 6558   Fn wfn 6559  ⟶wf 6560  ⟶1-1ontowf1o 6563  ‘cfv 6564   Isom wiso 6565  (class class class)co 7449   ∈ cmpo 7451  ωcom 7909   supp csupp 8212  seq_ωcseqom 8493   +_o coa 8509   ·_o comu 8510   ↑_o coe 8511   finSupp cfsupp 9389  OrdIsocoi 9538   CNF ccnf 9697

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-inf2 9677

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-se 5610  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-isom 6573  df-riota 7406  df-ov 7452  df-oprab 7453  df-mpo 7454  df-om 7910  df-1st 8033  df-2nd 8034  df-supp 8213  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-seqom 8494  df-1o 8512  df-2o 8513  df-oadd 8516  df-omul 8517  df-oexp 8518  df-er 8753  df-map 8885  df-en 9010  df-dom 9011  df-sdom 9012  df-fin 9013  df-fsupp 9390  df-oi 9539  df-cnf 9698

This theorem is used by:  cnfcom  9736