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

Theorem cnfcomlem 9150
Description: Lemma for cnfcom 9151. (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 9097 . . . . . . 7 ω ∈ On
2 cnfcom.a . . . . . . . 8 (𝜑𝐴 ∈ On)
3 suppssdm 7832 . . . . . . . . . 10 (𝐹 supp ∅) ⊆ dom 𝐹
4 cnfcom.f . . . . . . . . . . . . 13 𝐹 = ((ω CNF 𝐴)‘𝐵)
5 cnfcom.s . . . . . . . . . . . . . . . 16 𝑆 = dom (ω CNF 𝐴)
61a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ω ∈ On)
75, 6, 2cantnff1o 9147 . . . . . . . . . . . . . . 15 (𝜑 → (ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴))
8 f1ocnv 6620 . . . . . . . . . . . . . . 15 ((ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴) → (ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆)
9 f1of 6608 . . . . . . . . . . . . . . 15 ((ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
107, 8, 93syl 18 . . . . . . . . . . . . . 14 (𝜑(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11 cnfcom.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (ω ↑o 𝐴))
1210, 11ffvelrnd 6844 . . . . . . . . . . . . 13 (𝜑 → ((ω CNF 𝐴)‘𝐵) ∈ 𝑆)
134, 12eqeltrid 2914 . . . . . . . . . . . 12 (𝜑𝐹𝑆)
145, 6, 2cantnfs 9117 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
1513, 14mpbid 233 . . . . . . . . . . 11 (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
1615simpld 495 . . . . . . . . . 10 (𝜑𝐹:𝐴⟶ω)
173, 16fssdm 6523 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18 cnfcom.1 . . . . . . . . . 10 (𝜑𝐼 ∈ dom 𝐺)
19 cnfcom.g . . . . . . . . . . . 12 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 8982 . . . . . . . . . . 11 𝐺:dom 𝐺⟶(𝐹 supp ∅)
2120ffvelrni 6842 . . . . . . . . . 10 (𝐼 ∈ dom 𝐺 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2218, 21syl 17 . . . . . . . . 9 (𝜑 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2317, 22sseldd 3965 . . . . . . . 8 (𝜑 → (𝐺𝐼) ∈ 𝐴)
24 onelon 6209 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐺𝐼) ∈ 𝐴) → (𝐺𝐼) ∈ On)
252, 23, 24syl2anc 584 . . . . . . 7 (𝜑 → (𝐺𝐼) ∈ On)
26 oecl 8151 . . . . . . 7 ((ω ∈ On ∧ (𝐺𝐼) ∈ On) → (ω ↑o (𝐺𝐼)) ∈ On)
271, 25, 26sylancr 587 . . . . . 6 (𝜑 → (ω ↑o (𝐺𝐼)) ∈ On)
2816, 23ffvelrnd 6844 . . . . . . 7 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ ω)
29 nnon 7575 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ ω → (𝐹‘(𝐺𝐼)) ∈ On)
3028, 29syl 17 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ On)
31 omcl 8150 . . . . . 6 (((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
3227, 30, 31syl2anc 584 . . . . 5 (𝜑 → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
335, 6, 2, 19, 13cantnfcl 9118 . . . . . . . 8 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
3433simprd 496 . . . . . . 7 (𝜑 → dom 𝐺 ∈ ω)
35 elnn 7579 . . . . . . 7 ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
3618, 34, 35syl2anc 584 . . . . . 6 (𝜑𝐼 ∈ ω)
37 cnfcom.h . . . . . . . 8 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
3837cantnfvalf 9116 . . . . . . 7 𝐻:ω⟶On
3938ffvelrni 6842 . . . . . 6 (𝐼 ∈ ω → (𝐻𝐼) ∈ On)
4036, 39syl 17 . . . . 5 (𝜑 → (𝐻𝐼) ∈ On)
41 eqid 2818 . . . . . 6 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
4241oacomf1o 8180 . . . . 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 8082 . . . . . . 7 (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)))
4636, 45syl 17 . . . . . 6 (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)))
47 nfcv 2974 . . . . . . . . 9 𝑢𝐾
48 nfcv 2974 . . . . . . . . 9 𝑣𝐾
49 nfcv 2974 . . . . . . . . 9 𝑘((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
50 nfcv 2974 . . . . . . . . 9 𝑓((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
51 cnfcom.k . . . . . . . . . 10 𝐾 = ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52 oveq2 7153 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
5352cbvmptv 5160 . . . . . . . . . . . 12 (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦))
54 cnfcom.m . . . . . . . . . . . . . 14 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
55 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑘 = 𝑢)
5655fveq2d 6667 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐺𝑘) = (𝐺𝑢))
5756oveq2d 7161 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (ω ↑o (𝐺𝑘)) = (ω ↑o (𝐺𝑢)))
5856fveq2d 6667 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺𝑢)))
5957, 58oveq12d 7163 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
6054, 59syl5eq 2865 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
61 simpr 485 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑓 = 𝑣)
6261dmeqd 5767 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
6362oveq1d 7160 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
6460, 63mpteq12dv 5142 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
6553, 64syl5eq 2865 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66 oveq2 7153 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
6766cbvmptv 5160 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
6860oveq1d 7160 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))
6962, 68mpteq12dv 5142 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7067, 69syl5eq 2865 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7170cnveqd 5739 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7265, 71uneq12d 4137 . . . . . . . . . 10 ((𝑘 = 𝑢𝑓 = 𝑣) → ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7351, 72syl5eq 2865 . . . . . . . . 9 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7447, 48, 49, 50, 73cbvmpo 7237 . . . . . . . 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 767 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → 𝑢 = 𝐼)
7776fveq2d 6667 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐺𝑢) = (𝐺𝐼))
7877oveq2d 7161 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (ω ↑o (𝐺𝑢)) = (ω ↑o (𝐺𝐼)))
7977fveq2d 6667 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝐼)))
8078, 79oveq12d 7163 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
81 simpr 485 . . . . . . . . . . . 12 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → 𝑣 = (𝑇𝐼))
8281dmeqd 5767 . . . . . . . . . . 11 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → dom 𝑣 = dom (𝑇𝐼))
83 cnfcom.3 . . . . . . . . . . . 12 (𝜑 → (𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂)
84 f1odm 6612 . . . . . . . . . . . 12 ((𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂 → dom (𝑇𝐼) = (𝐻𝐼))
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → dom (𝑇𝐼) = (𝐻𝐼))
8682, 85sylan9eqr 2875 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → dom 𝑣 = (𝐻𝐼))
8786oveq1d 7160 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻𝐼) +o 𝑦))
8880, 87mpteq12dv 5142 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)))
8980oveq1d 7160 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))
9086, 89mpteq12dv 5142 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9190cnveqd 5739 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9288, 91uneq12d 4137 . . . . . . 7 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
9318elexd 3512 . . . . . . 7 (𝜑𝐼 ∈ V)
94 fvexd 6678 . . . . . . 7 (𝜑 → (𝑇𝐼) ∈ V)
95 ovex 7178 . . . . . . . . . 10 ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ V
9695mptex 6977 . . . . . . . . 9 (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∈ V
97 fvex 6676 . . . . . . . . . . 11 (𝐻𝐼) ∈ V
9897mptex 6977 . . . . . . . . . 10 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
9998cnvex 7619 . . . . . . . . 9 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
10096, 99unex 7458 . . . . . . . 8 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V
101100a1i 11 . . . . . . 7 (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V)
10275, 92, 93, 94, 101ovmpod 7291 . . . . . 6 (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
10346, 102eqtrd 2853 . . . . 5 (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
104 f1oeq1 6597 . . . . 5 ((𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) → ((𝑇‘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 (𝐹‘(𝐺𝐼))))))
105103, 104syl 17 . . . 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 (𝐹‘(𝐺𝐼))))))
10643, 105mpbird 258 . . 3 (𝜑 → (𝑇‘suc 𝐼):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
1071a1i 11 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → ω ∈ On)
108 simpl 483 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → 𝐴 ∈ On)
109 simpr 485 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → 𝐹𝑆)
11054oveq1i 7155 . . . . . . . . . 10 (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)
111110a1i 11 . . . . . . . . 9 ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧))
112111mpoeq3ia 7221 . . . . . . . 8 (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧))
113 eqid 2818 . . . . . . . 8 ∅ = ∅
114 seqomeq12 8079 . . . . . . . 8 (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)) ∧ ∅ = ∅) → seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅))
115112, 113, 114mp2an 688 . . . . . . 7 seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
11637, 115eqtri 2841 . . . . . 6 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
1175, 107, 108, 19, 109, 116cantnfsuc 9121 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
1182, 13, 36, 117syl21anc 833 . . . 4 (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
119118f1oeq2d 6604 . . 3 (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))))
120106, 119mpbird 258 . 2 (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
121 sssucid 6261 . . . . . 6 dom 𝐺 ⊆ suc dom 𝐺
122121, 18sseldi 3962 . . . . 5 (𝜑𝐼 ∈ suc dom 𝐺)
123 epelg 5459 . . . . . . . . . . 11 (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼𝑦𝐼))
12418, 123syl 17 . . . . . . . . . 10 (𝜑 → (𝑦 E 𝐼𝑦𝐼))
125124biimpar 478 . . . . . . . . 9 ((𝜑𝑦𝐼) → 𝑦 E 𝐼)
126 ovexd 7180 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ∈ V)
12733simpld 495 . . . . . . . . . . . 12 (𝜑 → E We (𝐹 supp ∅))
12819oiiso 8989 . . . . . . . . . . . 12 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
129126, 127, 128syl2anc 584 . . . . . . . . . . 11 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
130129adantr 481 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
13119oicl 8981 . . . . . . . . . . . 12 Ord dom 𝐺
132 ordelss 6200 . . . . . . . . . . . 12 ((Ord dom 𝐺𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
133131, 18, 132sylancr 587 . . . . . . . . . . 11 (𝜑𝐼 ⊆ dom 𝐺)
134133sselda 3964 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝑦 ∈ dom 𝐺)
13518adantr 481 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝐼 ∈ dom 𝐺)
136 isorel 7068 . . . . . . . . . 10 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
137130, 134, 135, 136syl12anc 832 . . . . . . . . 9 ((𝜑𝑦𝐼) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
138125, 137mpbid 233 . . . . . . . 8 ((𝜑𝑦𝐼) → (𝐺𝑦) E (𝐺𝐼))
139 fvex 6676 . . . . . . . . 9 (𝐺𝐼) ∈ V
140139epeli 5461 . . . . . . . 8 ((𝐺𝑦) E (𝐺𝐼) ↔ (𝐺𝑦) ∈ (𝐺𝐼))
141138, 140sylib 219 . . . . . . 7 ((𝜑𝑦𝐼) → (𝐺𝑦) ∈ (𝐺𝐼))
142141ralrimiva 3179 . . . . . 6 (𝜑 → ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼))
143 ffun 6510 . . . . . . . 8 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
14420, 143ax-mp 5 . . . . . . 7 Fun 𝐺
145 funimass4 6723 . . . . . . 7 ((Fun 𝐺𝐼 ⊆ dom 𝐺) → ((𝐺𝐼) ⊆ (𝐺𝐼) ↔ ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼)))
146144, 133, 145sylancr 587 . . . . . 6 (𝜑 → ((𝐺𝐼) ⊆ (𝐺𝐼) ↔ ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼)))
147142, 146mpbird 258 . . . . 5 (𝜑 → (𝐺𝐼) ⊆ (𝐺𝐼))
1481a1i 11 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → ω ∈ On)
149 simpll 763 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → 𝐴 ∈ On)
150 simplr 765 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → 𝐹𝑆)
151 peano1 7590 . . . . . . 7 ∅ ∈ ω
152151a1i 11 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → ∅ ∈ ω)
153 simpr1 1186 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → 𝐼 ∈ suc dom 𝐺)
154 simpr2 1187 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐺𝐼) ∈ On)
155 simpr3 1188 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐺𝐼) ⊆ (𝐺𝐼))
1565, 148, 149, 19, 150, 116, 152, 153, 154, 155cantnflt 9123 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
1572, 13, 122, 25, 147, 156syl23anc 1369 . . . 4 (𝜑 → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
15816ffnd 6508 . . . . . . . . 9 (𝜑𝐹 Fn 𝐴)
159 0ex 5202 . . . . . . . . . 10 ∅ ∈ V
160159a1i 11 . . . . . . . . 9 (𝜑 → ∅ ∈ V)
161 elsuppfn 7827 . . . . . . . . 9 ((𝐹 Fn 𝐴𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
162158, 2, 160, 161syl3anc 1363 . . . . . . . 8 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
163 simpr 485 . . . . . . . 8 (((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅)
164162, 163syl6bi 254 . . . . . . 7 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅))
16522, 164mpd 15 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ≠ ∅)
166 on0eln0 6239 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
16730, 166syl 17 . . . . . 6 (𝜑 → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
168165, 167mpbird 258 . . . . 5 (𝜑 → ∅ ∈ (𝐹‘(𝐺𝐼)))
169 omword1 8188 . . . . 5 ((((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺𝐼))) → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
17027, 30, 168, 169syl21anc 833 . . . 4 (𝜑 → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
171 oaabs2 8261 . . . 4 ((((𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)) ∧ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On) ∧ (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
172157, 32, 170, 171syl21anc 833 . . 3 (𝜑 → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
173172f1oeq3d 6605 . 2 (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
174120, 173mpbid 233 1 (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  Vcvv 3492  cun 3931  wss 3933  c0 4288   class class class wbr 5057  cmpt 5137   E cep 5457   We wwe 5506  ccnv 5547  dom cdm 5548  cima 5551  Ord word 6183  Oncon0 6184  suc csuc 6186  Fun wfun 6342   Fn wfn 6343  wf 6344  1-1-ontowf1o 6347  cfv 6348   Isom wiso 6349  (class class class)co 7145  cmpo 7147  ωcom 7569   supp csupp 7819  seqωcseqom 8072   +o coa 8088   ·o comu 8089  o coe 8090   finSupp cfsupp 8821  OrdIsocoi 8961   CNF ccnf 9112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-seqom 8073  df-1o 8091  df-2o 8092  df-oadd 8095  df-omul 8096  df-oexp 8097  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-oi 8962  df-cnf 9113
This theorem is referenced by:  cnfcom  9151
  Copyright terms: Public domain W3C validator