MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnfcomlem Structured version   Visualization version   GIF version

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.
StepHypRef 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 𝐴)
61a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ω ∈ On)
75, 6, 2cantnff1o 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 𝐴)⟶𝑆)
107, 8, 93syl 18 . . . . . . . . . . . . . 14 (𝜑(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11 cnfcom.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (ω ↑o 𝐴))
1210, 11ffvelcdmd 7036 . . . . . . . . . . . . 13 (𝜑 → ((ω CNF 𝐴)‘𝐵) ∈ 𝑆)
134, 12eqeltrid 2842 . . . . . . . . . . . 12 (𝜑𝐹𝑆)
145, 6, 2cantnfs 9602 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
1513, 14mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
1615simpld 495 . . . . . . . . . 10 (𝜑𝐹:𝐴⟶ω)
173, 16fssdm 6688 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18 cnfcom.1 . . . . . . . . . 10 (𝜑𝐼 ∈ dom 𝐺)
19 cnfcom.g . . . . . . . . . . . 12 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 9466 . . . . . . . . . . 11 𝐺:dom 𝐺⟶(𝐹 supp ∅)
2120ffvelcdmi 7034 . . . . . . . . . 10 (𝐼 ∈ dom 𝐺 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2218, 21syl 17 . . . . . . . . 9 (𝜑 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2317, 22sseldd 3945 . . . . . . . 8 (𝜑 → (𝐺𝐼) ∈ 𝐴)
24 onelon 6342 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐺𝐼) ∈ 𝐴) → (𝐺𝐼) ∈ On)
252, 23, 24syl2anc 584 . . . . . . 7 (𝜑 → (𝐺𝐼) ∈ On)
26 oecl 8483 . . . . . . 7 ((ω ∈ On ∧ (𝐺𝐼) ∈ On) → (ω ↑o (𝐺𝐼)) ∈ On)
271, 25, 26sylancr 587 . . . . . 6 (𝜑 → (ω ↑o (𝐺𝐼)) ∈ On)
2816, 23ffvelcdmd 7036 . . . . . . 7 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ ω)
29 nnon 7808 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ ω → (𝐹‘(𝐺𝐼)) ∈ On)
3028, 29syl 17 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ On)
31 omcl 8482 . . . . . 6 (((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
3227, 30, 31syl2anc 584 . . . . 5 (𝜑 → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
335, 6, 2, 19, 13cantnfcl 9603 . . . . . . . 8 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
3433simprd 496 . . . . . . 7 (𝜑 → dom 𝐺 ∈ ω)
35 elnn 7813 . . . . . . 7 ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
3618, 34, 35syl2anc 584 . . . . . 6 (𝜑𝐼 ∈ ω)
37 cnfcom.h . . . . . . . 8 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
3837cantnfvalf 9601 . . . . . . 7 𝐻:ω⟶On
3938ffvelcdmi 7034 . . . . . 6 (𝐼 ∈ ω → (𝐻𝐼) ∈ On)
4036, 39syl 17 . . . . 5 (𝜑 → (𝐻𝐼) ∈ On)
41 eqid 2736 . . . . . 6 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
4241oacomf1o 8512 . . . . 5 ((((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On ∧ (𝐻𝐼) ∈ On) → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
4332, 40, 42syl2anc 584 . . . 4 (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
44 cnfcom.t . . . . . . . 8 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
4544seqomsuc 8403 . . . . . . 7 (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)))
4636, 45syl 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 𝑦))
5352cbvmptv 5218 . . . . . . . . . . . 12 (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦))
54 cnfcom.m . . . . . . . . . . . . . 14 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
55 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑘 = 𝑢)
5655fveq2d 6846 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐺𝑘) = (𝐺𝑢))
5756oveq2d 7373 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (ω ↑o (𝐺𝑘)) = (ω ↑o (𝐺𝑢)))
5856fveq2d 6846 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺𝑢)))
5957, 58oveq12d 7375 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
6054, 59eqtrid 2788 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
61 simpr 485 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑓 = 𝑣)
6261dmeqd 5861 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
6362oveq1d 7372 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
6460, 63mpteq12dv 5196 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
6553, 64eqtrid 2788 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66 oveq2 7365 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
6766cbvmptv 5218 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
6860oveq1d 7372 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))
6962, 68mpteq12dv 5196 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7067, 69eqtrid 2788 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7170cnveqd 5831 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7265, 71uneq12d 4124 . . . . . . . . . 10 ((𝑘 = 𝑢𝑓 = 𝑣) → ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7351, 72eqtrid 2788 . . . . . . . . 9 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7447, 48, 49, 50, 73cbvmpo 7451 . . . . . . . 8 (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7574a1i 11 . . . . . . 7 (𝜑 → (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))))
76 simprl 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → 𝑢 = 𝐼)
7776fveq2d 6846 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐺𝑢) = (𝐺𝐼))
7877oveq2d 7373 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (ω ↑o (𝐺𝑢)) = (ω ↑o (𝐺𝐼)))
7977fveq2d 6846 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝐼)))
8078, 79oveq12d 7375 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
81 simpr 485 . . . . . . . . . . . 12 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → 𝑣 = (𝑇𝐼))
8281dmeqd 5861 . . . . . . . . . . 11 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → dom 𝑣 = dom (𝑇𝐼))
83 cnfcom.3 . . . . . . . . . . . 12 (𝜑 → (𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂)
84 f1odm 6788 . . . . . . . . . . . 12 ((𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂 → dom (𝑇𝐼) = (𝐻𝐼))
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → dom (𝑇𝐼) = (𝐻𝐼))
8682, 85sylan9eqr 2798 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → dom 𝑣 = (𝐻𝐼))
8786oveq1d 7372 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻𝐼) +o 𝑦))
8880, 87mpteq12dv 5196 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)))
8980oveq1d 7372 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))
9086, 89mpteq12dv 5196 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9190cnveqd 5831 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9288, 91uneq12d 4124 . . . . . . 7 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
9318elexd 3465 . . . . . . 7 (𝜑𝐼 ∈ V)
94 fvexd 6857 . . . . . . 7 (𝜑 → (𝑇𝐼) ∈ V)
95 ovex 7390 . . . . . . . . . 10 ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ V
9695mptex 7173 . . . . . . . . 9 (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∈ V
97 fvex 6855 . . . . . . . . . . 11 (𝐻𝐼) ∈ V
9897mptex 7173 . . . . . . . . . 10 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
9998cnvex 7862 . . . . . . . . 9 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
10096, 99unex 7680 . . . . . . . 8 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V
101100a1i 11 . . . . . . 7 (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V)
10275, 92, 93, 94, 101ovmpod 7507 . . . . . 6 (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
10346, 102eqtrd 2776 . . . . 5 (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
104103f1oeq1d 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 (𝐹‘(𝐺𝐼))))))
10543, 104mpbird 256 . . 3 (𝜑 → (𝑇‘suc 𝐼):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
1061a1i 11 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → ω ∈ On)
107 simpl 483 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → 𝐴 ∈ On)
108 simpr 485 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → 𝐹𝑆)
10954oveq1i 7367 . . . . . . . . . 10 (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)
110109a1i 11 . . . . . . . . 9 ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧))
111110mpoeq3ia 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 𝑧)), ∅))
114111, 112, 113mp2an 690 . . . . . . 7 seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
11537, 114eqtri 2764 . . . . . 6 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
1165, 106, 107, 19, 108, 115cantnfsuc 9606 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
1172, 13, 36, 116syl21anc 836 . . . 4 (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
118117f1oeq2d 6780 . . 3 (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))))
119105, 118mpbird 256 . 2 (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
120 sssucid 6397 . . . . . 6 dom 𝐺 ⊆ suc dom 𝐺
121120, 18sselid 3942 . . . . 5 (𝜑𝐼 ∈ suc dom 𝐺)
122 epelg 5538 . . . . . . . . . . 11 (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼𝑦𝐼))
12318, 122syl 17 . . . . . . . . . 10 (𝜑 → (𝑦 E 𝐼𝑦𝐼))
124123biimpar 478 . . . . . . . . 9 ((𝜑𝑦𝐼) → 𝑦 E 𝐼)
125 ovexd 7392 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ∈ V)
12633simpld 495 . . . . . . . . . . . 12 (𝜑 → E We (𝐹 supp ∅))
12719oiiso 9473 . . . . . . . . . . . 12 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
128125, 126, 127syl2anc 584 . . . . . . . . . . 11 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
129128adantr 481 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
13019oicl 9465 . . . . . . . . . . . 12 Ord dom 𝐺
131 ordelss 6333 . . . . . . . . . . . 12 ((Ord dom 𝐺𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
132130, 18, 131sylancr 587 . . . . . . . . . . 11 (𝜑𝐼 ⊆ dom 𝐺)
133132sselda 3944 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝑦 ∈ dom 𝐺)
13418adantr 481 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝐼 ∈ dom 𝐺)
135 isorel 7271 . . . . . . . . . 10 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
136129, 133, 134, 135syl12anc 835 . . . . . . . . 9 ((𝜑𝑦𝐼) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
137124, 136mpbid 231 . . . . . . . 8 ((𝜑𝑦𝐼) → (𝐺𝑦) E (𝐺𝐼))
138 fvex 6855 . . . . . . . . 9 (𝐺𝐼) ∈ V
139138epeli 5539 . . . . . . . 8 ((𝐺𝑦) E (𝐺𝐼) ↔ (𝐺𝑦) ∈ (𝐺𝐼))
140137, 139sylib 217 . . . . . . 7 ((𝜑𝑦𝐼) → (𝐺𝑦) ∈ (𝐺𝐼))
141140ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼))
142 ffun 6671 . . . . . . . 8 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
14320, 142ax-mp 5 . . . . . . 7 Fun 𝐺
144 funimass4 6907 . . . . . . 7 ((Fun 𝐺𝐼 ⊆ dom 𝐺) → ((𝐺𝐼) ⊆ (𝐺𝐼) ↔ ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼)))
145143, 132, 144sylancr 587 . . . . . 6 (𝜑 → ((𝐺𝐼) ⊆ (𝐺𝐼) ↔ ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼)))
146141, 145mpbird 256 . . . . 5 (𝜑 → (𝐺𝐼) ⊆ (𝐺𝐼))
1471a1i 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 ∅ ∈ ω
151150a1i 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 ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐺𝐼) ⊆ (𝐺𝐼))
1555, 147, 148, 19, 149, 115, 151, 152, 153, 154cantnflt 9608 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
1562, 13, 121, 25, 146, 155syl23anc 1377 . . . 4 (𝜑 → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
15716ffnd 6669 . . . . . . . . 9 (𝜑𝐹 Fn 𝐴)
158 0ex 5264 . . . . . . . . . 10 ∅ ∈ V
159158a1i 11 . . . . . . . . 9 (𝜑 → ∅ ∈ V)
160 elsuppfn 8102 . . . . . . . . 9 ((𝐹 Fn 𝐴𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
161157, 2, 159, 160syl3anc 1371 . . . . . . . 8 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
162 simpr 485 . . . . . . . 8 (((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅)
163161, 162syl6bi 252 . . . . . . 7 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅))
16422, 163mpd 15 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ≠ ∅)
165 on0eln0 6373 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
16630, 165syl 17 . . . . . 6 (𝜑 → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
167164, 166mpbird 256 . . . . 5 (𝜑 → ∅ ∈ (𝐹‘(𝐺𝐼)))
168 omword1 8520 . . . . 5 ((((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺𝐼))) → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
16927, 30, 167, 168syl21anc 836 . . . 4 (𝜑 → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
170 oaabs2 8595 . . . 4 ((((𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)) ∧ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On) ∧ (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
171156, 32, 169, 170syl21anc 836 . . 3 (𝜑 → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
172171f1oeq3d 6781 . 2 (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
173119, 172mpbid 231 1 (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
Colors of variables: wff setvar class
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-ontowf1o 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
  Copyright terms: Public domain W3C validator