Theorem cnfcomlem 9652

Description: Lemma for cnfcom 9653. (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 9599	. . . . . . 7 ⊢ ω ∈ On
2		cnfcom.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ On)
3		suppssdm 8156	. . . . . . . . . 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 9649	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
8		f1ocnv 6812	. . . . . . . . . . . . . . 15 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
9		f1of 6800	. . . . . . . . . . . . . . 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 7057	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
13	4, 12	eqeltrid 2832	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
14	5, 6, 2	cantnfs 9619	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
15	13, 14	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
16	15	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
17	3, 16	fssdm 6707	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18		cnfcom.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ dom 𝐺)
19		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
20	19	oif 9483	. . . . . . . . . . 11 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21	20	ffvelcdmi 7055	. . . . . . . . . 10 ⊢ (𝐼 ∈ dom 𝐺 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
22	18, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐼) ∈ (𝐹 supp ∅))
23	17, 22	sseldd 3947	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐴)
24		onelon 6357	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ (𝐺‘𝐼) ∈ 𝐴) → (𝐺‘𝐼) ∈ On)
25	2, 23, 24	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐼) ∈ On)
26		oecl 8501	. . . . . . 7 ⊢ ((ω ∈ On ∧ (𝐺‘𝐼) ∈ On) → (ω ↑o (𝐺‘𝐼)) ∈ On)
27	1, 25, 26	sylancr 587	. . . . . 6 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ∈ On)
28	16, 23	ffvelcdmd 7057	. . . . . . 7 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ ω)
29		nnon 7848	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ ω → (𝐹‘(𝐺‘𝐼)) ∈ On)
30	28, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ On)
31		omcl 8500	. . . . . 6 ⊢ (((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
32	27, 30, 31	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On)
33	5, 6, 2, 19, 13	cantnfcl 9620	. . . . . . . 8 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
34	33	simprd 495	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 ∈ ω)
35		elnn 7853	. . . . . . 7 ⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
36	18, 34, 35	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ω)
37		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
38	37	cantnfvalf 9618	. . . . . . 7 ⊢ 𝐻:ω⟶On
39	38	ffvelcdmi 7055	. . . . . 6 ⊢ (𝐼 ∈ ω → (𝐻‘𝐼) ∈ On)
40	36, 39	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻‘𝐼) ∈ On)
41		eqid 2729	. . . . . 6 ⊢ ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
42	41	oacomf1o 8529	. . . . 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 8425	. . . . . . 7 ⊢ (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
46	36, 45	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)))
47		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑢𝐾
48		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑣𝐾
49		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
50		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑓((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
51		cnfcom.k	. . . . . . . . . 10 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52		oveq2 7395	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
53	52	cbvmptv 5211	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦))
54		cnfcom.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))
55		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑘 = 𝑢)
56	55	fveq2d 6862	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐺‘𝑘) = (𝐺‘𝑢))
57	56	oveq2d 7403	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (ω ↑o (𝐺‘𝑘)) = (ω ↑o (𝐺‘𝑢)))
58	56	fveq2d 6862	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑢)))
59	57, 58	oveq12d 7405	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
60	54, 59	eqtrid 2776	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))))
61		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑓 = 𝑣)
62	61	dmeqd 5869	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
63	62	oveq1d 7402	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
64	60, 63	mpteq12dv 5194	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
65	53, 64	eqtrid 2776	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66		oveq2 7395	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
67	66	cbvmptv 5211	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
68	60	oveq1d 7402	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))
69	62, 68	mpteq12dv 5194	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
70	67, 69	eqtrid 2776	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
71	70	cnveqd 5839	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)))
72	65, 71	uneq12d 4132	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
73	51, 72	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))))
74	47, 48, 49, 50, 73	cbvmpo 7483	. . . . . . . 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 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → 𝑢 = 𝐼)
77	76	fveq2d 6862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐺‘𝑢) = (𝐺‘𝐼))
78	77	oveq2d 7403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (ω ↑o (𝐺‘𝑢)) = (ω ↑o (𝐺‘𝐼)))
79	77	fveq2d 6862	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝐼)))
80	78, 79	oveq12d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
81		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → 𝑣 = (𝑇‘𝐼))
82	81	dmeqd 5869	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → dom 𝑣 = dom (𝑇‘𝐼))
83		cnfcom.3	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)
84		f1odm 6804	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑇‘𝐼) = (𝐻‘𝐼))
86	82, 85	sylan9eqr 2786	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → dom 𝑣 = (𝐻‘𝐼))
87	86	oveq1d 7402	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻‘𝐼) +o 𝑦))
88	80, 87	mpteq12dv 5194	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)))
89	80	oveq1d 7402	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))
90	86, 89	mpteq12dv 5194	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
91	90	cnveqd 5839	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦)) = ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)))
92	88, 91	uneq12d 4132	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺‘𝑢)) ·o (𝐹‘(𝐺‘𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
93	18	elexd 3471	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
94		fvexd 6873	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝐼) ∈ V)
95		ovex 7420	. . . . . . . . . 10 ⊢ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ V
96	95	mptex 7197	. . . . . . . . 9 ⊢ (𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∈ V
97		fvex 6871	. . . . . . . . . . 11 ⊢ (𝐻‘𝐼) ∈ V
98	97	mptex 7197	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
99	98	cnvex 7901	. . . . . . . . 9 ⊢ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦)) ∈ V
100	96, 99	unex 7720	. . . . . . . 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 7541	. . . . . 6 ⊢ (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
103	46, 102	eqtrd 2764	. . . . 5 ⊢ (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +o 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o 𝑦))))
104	103	f1oeq1d 6795	. . . 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 257	. . 3 ⊢ (𝜑 → (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
106	1	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → ω ∈ On)
107		simpl 482	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐴 ∈ On)
108		simpr 484	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐹 ∈ 𝑆)
109	54	oveq1i 7397	. . . . . . . . . 10 ⊢ (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)
110	109	a1i 11	. . . . . . . . 9 ⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
111	110	mpoeq3ia 7467	. . . . . . . 8 ⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))
112		eqid 2729	. . . . . . . 8 ⊢ ∅ = ∅
113		seqomeq12 8422	. . . . . . . 8 ⊢ (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ∧ ∅ = ∅) → seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅))
114	111, 112, 113	mp2an 692	. . . . . . 7 ⊢ seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
115	37, 114	eqtri 2752	. . . . . 6 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)
116	5, 106, 107, 19, 108, 115	cantnfsuc 9623	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
117	2, 13, 36, 116	syl21anc 837	. . . 4 ⊢ (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼)))
118	117	f1oeq2d 6796	. . 3 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) +o (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))))
119	105, 118	mpbird 257	. 2 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
120		sssucid 6414	. . . . . 6 ⊢ dom 𝐺 ⊆ suc dom 𝐺
121	120, 18	sselid 3944	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ suc dom 𝐺)
122		epelg 5539	. . . . . . . . . . 11 ⊢ (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
123	18, 122	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼))
124	123	biimpar 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 E 𝐼)
125		ovexd 7422	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
126	33	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → E We (𝐹 supp ∅))
127	19	oiiso 9490	. . . . . . . . . . . 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 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
130	19	oicl 9482	. . . . . . . . . . . 12 ⊢ Ord dom 𝐺
131		ordelss 6348	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
132	130, 18, 131	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ⊆ dom 𝐺)
133	132	sselda 3946	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ dom 𝐺)
134	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ dom 𝐺)
135		isorel 7301	. . . . . . . . . 10 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ 𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
136	129, 133, 134, 135	syl12anc 836	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼)))
137	124, 136	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) E (𝐺‘𝐼))
138		fvex 6871	. . . . . . . . 9 ⊢ (𝐺‘𝐼) ∈ V
139	138	epeli 5540	. . . . . . . 8 ⊢ ((𝐺‘𝑦) E (𝐺‘𝐼) ↔ (𝐺‘𝑦) ∈ (𝐺‘𝐼))
140	137, 139	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ (𝐺‘𝐼))
141	140	ralrimiva 3125	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))
142		ffun 6691	. . . . . . . 8 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
143	20, 142	ax-mp 5	. . . . . . 7 ⊢ Fun 𝐺
144		funimass4 6925	. . . . . . 7 ⊢ ((Fun 𝐺 ∧ 𝐼 ⊆ dom 𝐺) → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
145	143, 132, 144	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)))
146	141, 145	mpbird 257	. . . . 5 ⊢ (𝜑 → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
147	1	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ω ∈ On)
148		simpll 766	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐴 ∈ On)
149		simplr 768	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐹 ∈ 𝑆)
150		peano1 7865	. . . . . . 7 ⊢ ∅ ∈ ω
151	150	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ∅ ∈ ω)
152		simpr1 1195	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐼 ∈ suc dom 𝐺)
153		simpr2 1196	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺‘𝐼) ∈ On)
154		simpr3 1197	. . . . . 6 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))
155	5, 147, 148, 19, 149, 115, 151, 152, 153, 154	cantnflt 9625	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
156	2, 13, 121, 25, 146, 155	syl23anc 1379	. . . 4 ⊢ (𝜑 → (𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)))
157	16	ffnd 6689	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐴)
158		0ex 5262	. . . . . . . . . 10 ⊢ ∅ ∈ V
159	158	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ V)
160		elsuppfn 8149	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
161	157, 2, 159, 160	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅)))
162		simpr 484	. . . . . . . 8 ⊢ (((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
163	161, 162	biimtrdi 253	. . . . . . 7 ⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅))
164	22, 163	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ≠ ∅)
165		on0eln0 6389	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
166	30, 165	syl 17	. . . . . 6 ⊢ (𝜑 → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅))
167	164, 166	mpbird 257	. . . . 5 ⊢ (𝜑 → ∅ ∈ (𝐹‘(𝐺‘𝐼)))
168		omword1 8537	. . . . 5 ⊢ ((((ω ↑o (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺‘𝐼))) → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
169	27, 30, 167, 168	syl21anc 837	. . . 4 ⊢ (𝜑 → (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
170		oaabs2 8613	. . . 4 ⊢ ((((𝐻‘𝐼) ∈ (ω ↑o (𝐺‘𝐼)) ∧ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))) ∈ On) ∧ (ω ↑o (𝐺‘𝐼)) ⊆ ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) → ((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
171	156, 32, 169, 170	syl21anc 837	. . 3 ⊢ (𝜑 → ((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
172	171	f1oeq3d 6797	. 2 ⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +o ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))
173	119, 172	mpbid 232	1 ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  Vcvv 3447   ∪ cun 3912   ⊆ wss 3914  ∅c0 4296   class class class wbr 5107   ↦ cmpt 5188   E cep 5537   We wwe 5590  ^◡ccnv 5637  dom cdm 5638   “ cima 5641  Ord word 6331  Oncon0 6332  suc csuc 6334  Fun wfun 6505   Fn wfn 6506  ⟶wf 6507  –1-1-onto→wf1o 6510  ‘cfv 6511   Isom wiso 6512  (class class class)co 7387   ∈ cmpo 7389  ωcom 7842   supp csupp 8139  seq_ωcseqom 8415   +_o coa 8431   ·_o comu 8432   ↑_o coe 8433   finSupp cfsupp 9312  OrdIsocoi 9462   CNF ccnf 9614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-supp 8140  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-seqom 8416  df-1o 8434  df-2o 8435  df-oadd 8438  df-omul 8439  df-oexp 8440  df-er 8671  df-map 8801  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-fsupp 9313  df-oi 9463  df-cnf 9615

This theorem is referenced by:  cnfcom  9653