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

Theorem cnfcomlem 9148
 Description: Lemma for cnfcom 9149. (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 9095 . . . . . . 7 ω ∈ On
2 cnfcom.a . . . . . . . 8 (𝜑𝐴 ∈ On)
3 suppssdm 7828 . . . . . . . . . 10 (𝐹 supp ∅) ⊆ dom 𝐹
4 cnfcom.f . . . . . . . . . . . . 13 𝐹 = ((ω CNF 𝐴)‘𝐵)
5 cnfcom.s . . . . . . . . . . . . . . . 16 𝑆 = dom (ω CNF 𝐴)
61a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ω ∈ On)
75, 6, 2cantnff1o 9145 . . . . . . . . . . . . . . 15 (𝜑 → (ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴))
8 f1ocnv 6602 . . . . . . . . . . . . . . 15 ((ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴) → (ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆)
9 f1of 6590 . . . . . . . . . . . . . . 15 ((ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
107, 8, 93syl 18 . . . . . . . . . . . . . 14 (𝜑(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11 cnfcom.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (ω ↑o 𝐴))
1210, 11ffvelrnd 6829 . . . . . . . . . . . . 13 (𝜑 → ((ω CNF 𝐴)‘𝐵) ∈ 𝑆)
134, 12eqeltrid 2894 . . . . . . . . . . . 12 (𝜑𝐹𝑆)
145, 6, 2cantnfs 9115 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
1513, 14mpbid 235 . . . . . . . . . . 11 (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
1615simpld 498 . . . . . . . . . 10 (𝜑𝐹:𝐴⟶ω)
173, 16fssdm 6504 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18 cnfcom.1 . . . . . . . . . 10 (𝜑𝐼 ∈ dom 𝐺)
19 cnfcom.g . . . . . . . . . . . 12 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 8980 . . . . . . . . . . 11 𝐺:dom 𝐺⟶(𝐹 supp ∅)
2120ffvelrni 6827 . . . . . . . . . 10 (𝐼 ∈ dom 𝐺 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2218, 21syl 17 . . . . . . . . 9 (𝜑 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2317, 22sseldd 3916 . . . . . . . 8 (𝜑 → (𝐺𝐼) ∈ 𝐴)
24 onelon 6184 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐺𝐼) ∈ 𝐴) → (𝐺𝐼) ∈ On)
252, 23, 24syl2anc 587 . . . . . . 7 (𝜑 → (𝐺𝐼) ∈ On)
26 oecl 8147 . . . . . . 7 ((ω ∈ On ∧ (𝐺𝐼) ∈ On) → (ω ↑o (𝐺𝐼)) ∈ On)
271, 25, 26sylancr 590 . . . . . 6 (𝜑 → (ω ↑o (𝐺𝐼)) ∈ On)
2816, 23ffvelrnd 6829 . . . . . . 7 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ ω)
29 nnon 7568 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ ω → (𝐹‘(𝐺𝐼)) ∈ On)
3028, 29syl 17 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ On)
31 omcl 8146 . . . . . 6 (((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
3227, 30, 31syl2anc 587 . . . . 5 (𝜑 → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
335, 6, 2, 19, 13cantnfcl 9116 . . . . . . . 8 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
3433simprd 499 . . . . . . 7 (𝜑 → dom 𝐺 ∈ ω)
35 elnn 7572 . . . . . . 7 ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
3618, 34, 35syl2anc 587 . . . . . 6 (𝜑𝐼 ∈ ω)
37 cnfcom.h . . . . . . . 8 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
3837cantnfvalf 9114 . . . . . . 7 𝐻:ω⟶On
3938ffvelrni 6827 . . . . . 6 (𝐼 ∈ ω → (𝐻𝐼) ∈ On)
4036, 39syl 17 . . . . 5 (𝜑 → (𝐻𝐼) ∈ On)
41 eqid 2798 . . . . . 6 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
4241oacomf1o 8176 . . . . 5 ((((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On ∧ (𝐻𝐼) ∈ On) → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
4332, 40, 42syl2anc 587 . . . 4 (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
44 cnfcom.t . . . . . . . 8 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
4544seqomsuc 8078 . . . . . . 7 (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)))
4636, 45syl 17 . . . . . 6 (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)))
47 nfcv 2955 . . . . . . . . 9 𝑢𝐾
48 nfcv 2955 . . . . . . . . 9 𝑣𝐾
49 nfcv 2955 . . . . . . . . 9 𝑘((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
50 nfcv 2955 . . . . . . . . 9 𝑓((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
51 cnfcom.k . . . . . . . . . 10 𝐾 = ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52 oveq2 7143 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
5352cbvmptv 5133 . . . . . . . . . . . 12 (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦))
54 cnfcom.m . . . . . . . . . . . . . 14 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
55 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑘 = 𝑢)
5655fveq2d 6649 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐺𝑘) = (𝐺𝑢))
5756oveq2d 7151 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (ω ↑o (𝐺𝑘)) = (ω ↑o (𝐺𝑢)))
5856fveq2d 6649 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺𝑢)))
5957, 58oveq12d 7153 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
6054, 59syl5eq 2845 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
61 simpr 488 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑓 = 𝑣)
6261dmeqd 5738 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
6362oveq1d 7150 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
6460, 63mpteq12dv 5115 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
6553, 64syl5eq 2845 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66 oveq2 7143 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
6766cbvmptv 5133 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
6860oveq1d 7150 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))
6962, 68mpteq12dv 5115 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7067, 69syl5eq 2845 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7170cnveqd 5710 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7265, 71uneq12d 4091 . . . . . . . . . 10 ((𝑘 = 𝑢𝑓 = 𝑣) → ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7351, 72syl5eq 2845 . . . . . . . . 9 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7447, 48, 49, 50, 73cbvmpo 7227 . . . . . . . 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 770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → 𝑢 = 𝐼)
7776fveq2d 6649 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐺𝑢) = (𝐺𝐼))
7877oveq2d 7151 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (ω ↑o (𝐺𝑢)) = (ω ↑o (𝐺𝐼)))
7977fveq2d 6649 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝐼)))
8078, 79oveq12d 7153 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
81 simpr 488 . . . . . . . . . . . 12 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → 𝑣 = (𝑇𝐼))
8281dmeqd 5738 . . . . . . . . . . 11 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → dom 𝑣 = dom (𝑇𝐼))
83 cnfcom.3 . . . . . . . . . . . 12 (𝜑 → (𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂)
84 f1odm 6594 . . . . . . . . . . . 12 ((𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂 → dom (𝑇𝐼) = (𝐻𝐼))
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → dom (𝑇𝐼) = (𝐻𝐼))
8682, 85sylan9eqr 2855 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → dom 𝑣 = (𝐻𝐼))
8786oveq1d 7150 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻𝐼) +o 𝑦))
8880, 87mpteq12dv 5115 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)))
8980oveq1d 7150 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))
9086, 89mpteq12dv 5115 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9190cnveqd 5710 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9288, 91uneq12d 4091 . . . . . . 7 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
9318elexd 3461 . . . . . . 7 (𝜑𝐼 ∈ V)
94 fvexd 6660 . . . . . . 7 (𝜑 → (𝑇𝐼) ∈ V)
95 ovex 7168 . . . . . . . . . 10 ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ V
9695mptex 6963 . . . . . . . . 9 (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∈ V
97 fvex 6658 . . . . . . . . . . 11 (𝐻𝐼) ∈ V
9897mptex 6963 . . . . . . . . . 10 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
9998cnvex 7614 . . . . . . . . 9 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
10096, 99unex 7451 . . . . . . . 8 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V
101100a1i 11 . . . . . . 7 (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V)
10275, 92, 93, 94, 101ovmpod 7282 . . . . . 6 (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
10346, 102eqtrd 2833 . . . . 5 (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
104 f1oeq1 6579 . . . . 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 260 . . 3 (𝜑 → (𝑇‘suc 𝐼):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
1071a1i 11 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → ω ∈ On)
108 simpl 486 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → 𝐴 ∈ On)
109 simpr 488 . . . . . 6 ((𝐴 ∈ On ∧ 𝐹𝑆) → 𝐹𝑆)
11054oveq1i 7145 . . . . . . . . . 10 (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)
111110a1i 11 . . . . . . . . 9 ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧))
112111mpoeq3ia 7211 . . . . . . . 8 (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧))
113 eqid 2798 . . . . . . . 8 ∅ = ∅
114 seqomeq12 8075 . . . . . . . 8 (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)) ∧ ∅ = ∅) → seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅))
115112, 113, 114mp2an 691 . . . . . . 7 seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
11637, 115eqtri 2821 . . . . . 6 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
1175, 107, 108, 19, 109, 116cantnfsuc 9119 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
1182, 13, 36, 117syl21anc 836 . . . 4 (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
119118f1oeq2d 6586 . . 3 (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼))–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))))
120106, 119mpbird 260 . 2 (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
121 sssucid 6236 . . . . . 6 dom 𝐺 ⊆ suc dom 𝐺
122121, 18sseldi 3913 . . . . 5 (𝜑𝐼 ∈ suc dom 𝐺)
123 epelg 5431 . . . . . . . . . . 11 (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼𝑦𝐼))
12418, 123syl 17 . . . . . . . . . 10 (𝜑 → (𝑦 E 𝐼𝑦𝐼))
125124biimpar 481 . . . . . . . . 9 ((𝜑𝑦𝐼) → 𝑦 E 𝐼)
126 ovexd 7170 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ∈ V)
12733simpld 498 . . . . . . . . . . . 12 (𝜑 → E We (𝐹 supp ∅))
12819oiiso 8987 . . . . . . . . . . . 12 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
129126, 127, 128syl2anc 587 . . . . . . . . . . 11 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
130129adantr 484 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
13119oicl 8979 . . . . . . . . . . . 12 Ord dom 𝐺
132 ordelss 6175 . . . . . . . . . . . 12 ((Ord dom 𝐺𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
133131, 18, 132sylancr 590 . . . . . . . . . . 11 (𝜑𝐼 ⊆ dom 𝐺)
134133sselda 3915 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝑦 ∈ dom 𝐺)
13518adantr 484 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝐼 ∈ dom 𝐺)
136 isorel 7058 . . . . . . . . . 10 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
137130, 134, 135, 136syl12anc 835 . . . . . . . . 9 ((𝜑𝑦𝐼) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
138125, 137mpbid 235 . . . . . . . 8 ((𝜑𝑦𝐼) → (𝐺𝑦) E (𝐺𝐼))
139 fvex 6658 . . . . . . . . 9 (𝐺𝐼) ∈ V
140139epeli 5432 . . . . . . . 8 ((𝐺𝑦) E (𝐺𝐼) ↔ (𝐺𝑦) ∈ (𝐺𝐼))
141138, 140sylib 221 . . . . . . 7 ((𝜑𝑦𝐼) → (𝐺𝑦) ∈ (𝐺𝐼))
142141ralrimiva 3149 . . . . . 6 (𝜑 → ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼))
143 ffun 6490 . . . . . . . 8 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
14420, 143ax-mp 5 . . . . . . 7 Fun 𝐺
145 funimass4 6705 . . . . . . 7 ((Fun 𝐺𝐼 ⊆ dom 𝐺) → ((𝐺𝐼) ⊆ (𝐺𝐼) ↔ ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼)))
146144, 133, 145sylancr 590 . . . . . 6 (𝜑 → ((𝐺𝐼) ⊆ (𝐺𝐼) ↔ ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼)))
147142, 146mpbird 260 . . . . 5 (𝜑 → (𝐺𝐼) ⊆ (𝐺𝐼))
1481a1i 11 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → ω ∈ On)
149 simpll 766 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → 𝐴 ∈ On)
150 simplr 768 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → 𝐹𝑆)
151 peano1 7583 . . . . . . 7 ∅ ∈ ω
152151a1i 11 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → ∅ ∈ ω)
153 simpr1 1191 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → 𝐼 ∈ suc dom 𝐺)
154 simpr2 1192 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐺𝐼) ∈ On)
155 simpr3 1193 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐺𝐼) ⊆ (𝐺𝐼))
1565, 148, 149, 19, 150, 116, 152, 153, 154, 155cantnflt 9121 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
1572, 13, 122, 25, 147, 156syl23anc 1374 . . . 4 (𝜑 → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
15816ffnd 6488 . . . . . . . . 9 (𝜑𝐹 Fn 𝐴)
159 0ex 5175 . . . . . . . . . 10 ∅ ∈ V
160159a1i 11 . . . . . . . . 9 (𝜑 → ∅ ∈ V)
161 elsuppfn 7823 . . . . . . . . 9 ((𝐹 Fn 𝐴𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
162158, 2, 160, 161syl3anc 1368 . . . . . . . 8 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
163 simpr 488 . . . . . . . 8 (((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅)
164162, 163syl6bi 256 . . . . . . 7 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅))
16522, 164mpd 15 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ≠ ∅)
166 on0eln0 6214 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
16730, 166syl 17 . . . . . 6 (𝜑 → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
168165, 167mpbird 260 . . . . 5 (𝜑 → ∅ ∈ (𝐹‘(𝐺𝐼)))
169 omword1 8184 . . . . 5 ((((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺𝐼))) → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
17027, 30, 168, 169syl21anc 836 . . . 4 (𝜑 → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
171 oaabs2 8257 . . . 4 ((((𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)) ∧ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On) ∧ (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
172157, 32, 170, 171syl21anc 836 . . 3 (𝜑 → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
173172f1oeq3d 6587 . 2 (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))))
174120, 173mpbid 235 1 (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243   class class class wbr 5030   ↦ cmpt 5110   E cep 5429   We wwe 5477  ◡ccnv 5518  dom cdm 5519   “ cima 5522  Ord word 6158  Oncon0 6159  suc csuc 6161  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  –1-1-onto→wf1o 6323  ‘cfv 6324   Isom wiso 6325  (class class class)co 7135   ∈ cmpo 7137  ωcom 7562   supp csupp 7815  seqωcseqom 8068   +o coa 8084   ·o comu 8085   ↑o coe 8086   finSupp cfsupp 8819  OrdIsocoi 8959   CNF ccnf 9110 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-supp 7816  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-seqom 8069  df-1o 8087  df-2o 8088  df-oadd 8091  df-omul 8092  df-oexp 8093  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-fsupp 8820  df-oi 8960  df-cnf 9111 This theorem is referenced by:  cnfcom  9149
 Copyright terms: Public domain W3C validator