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

Theorem cnfcomlem 9008
Description: Lemma for cnfcom 9009. (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 8955 . . . . . . 7 ω ∈ On
2 cnfcom.a . . . . . . . 8 (𝜑𝐴 ∈ On)
3 suppssdm 7694 . . . . . . . . . 10 (𝐹 supp ∅) ⊆ dom 𝐹
4 cnfcom.f . . . . . . . . . . . . 13 𝐹 = ((ω CNF 𝐴)‘𝐵)
5 cnfcom.s . . . . . . . . . . . . . . . 16 𝑆 = dom (ω CNF 𝐴)
61a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ω ∈ On)
75, 6, 2cantnff1o 9005 . . . . . . . . . . . . . . 15 (𝜑 → (ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴))
8 f1ocnv 6495 . . . . . . . . . . . . . . 15 ((ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴) → (ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆)
9 f1of 6483 . . . . . . . . . . . . . . 15 ((ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
107, 8, 93syl 18 . . . . . . . . . . . . . 14 (𝜑(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11 cnfcom.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (ω ↑o 𝐴))
1210, 11ffvelrnd 6717 . . . . . . . . . . . . 13 (𝜑 → ((ω CNF 𝐴)‘𝐵) ∈ 𝑆)
134, 12syl5eqel 2887 . . . . . . . . . . . 12 (𝜑𝐹𝑆)
145, 6, 2cantnfs 8975 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
1513, 14mpbid 233 . . . . . . . . . . 11 (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
1615simpld 495 . . . . . . . . . 10 (𝜑𝐹:𝐴⟶ω)
173, 16fssdm 6398 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18 cnfcom.1 . . . . . . . . . 10 (𝜑𝐼 ∈ dom 𝐺)
19 cnfcom.g . . . . . . . . . . . 12 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 8840 . . . . . . . . . . 11 𝐺:dom 𝐺⟶(𝐹 supp ∅)
2120ffvelrni 6715 . . . . . . . . . 10 (𝐼 ∈ dom 𝐺 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2218, 21syl 17 . . . . . . . . 9 (𝜑 → (𝐺𝐼) ∈ (𝐹 supp ∅))
2317, 22sseldd 3890 . . . . . . . 8 (𝜑 → (𝐺𝐼) ∈ 𝐴)
24 onelon 6091 . . . . . . . 8 ((𝐴 ∈ On ∧ (𝐺𝐼) ∈ 𝐴) → (𝐺𝐼) ∈ On)
252, 23, 24syl2anc 584 . . . . . . 7 (𝜑 → (𝐺𝐼) ∈ On)
26 oecl 8013 . . . . . . 7 ((ω ∈ On ∧ (𝐺𝐼) ∈ On) → (ω ↑o (𝐺𝐼)) ∈ On)
271, 25, 26sylancr 587 . . . . . 6 (𝜑 → (ω ↑o (𝐺𝐼)) ∈ On)
2816, 23ffvelrnd 6717 . . . . . . 7 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ ω)
29 nnon 7442 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ ω → (𝐹‘(𝐺𝐼)) ∈ On)
3028, 29syl 17 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ∈ On)
31 omcl 8012 . . . . . 6 (((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
3227, 30, 31syl2anc 584 . . . . 5 (𝜑 → ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On)
335, 6, 2, 19, 13cantnfcl 8976 . . . . . . . 8 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
3433simprd 496 . . . . . . 7 (𝜑 → dom 𝐺 ∈ ω)
35 elnn 7446 . . . . . . 7 ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω)
3618, 34, 35syl2anc 584 . . . . . 6 (𝜑𝐼 ∈ ω)
37 cnfcom.h . . . . . . . 8 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
3837cantnfvalf 8974 . . . . . . 7 𝐻:ω⟶On
3938ffvelrni 6715 . . . . . 6 (𝐼 ∈ ω → (𝐻𝐼) ∈ On)
4036, 39syl 17 . . . . 5 (𝜑 → (𝐻𝐼) ∈ On)
41 eqid 2795 . . . . . 6 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
4241oacomf1o 8041 . . . . 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 7944 . . . . . . 7 (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)))
4636, 45syl 17 . . . . . 6 (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)))
47 nfcv 2949 . . . . . . . . 9 𝑢𝐾
48 nfcv 2949 . . . . . . . . 9 𝑣𝐾
49 nfcv 2949 . . . . . . . . 9 𝑘((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
50 nfcv 2949 . . . . . . . . 9 𝑓((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
51 cnfcom.k . . . . . . . . . 10 𝐾 = ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
52 oveq2 7024 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (dom 𝑓 +o 𝑥) = (dom 𝑓 +o 𝑦))
5352cbvmptv 5061 . . . . . . . . . . . 12 (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦))
54 cnfcom.m . . . . . . . . . . . . . 14 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
55 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑘 = 𝑢)
5655fveq2d 6542 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐺𝑘) = (𝐺𝑢))
5756oveq2d 7032 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (ω ↑o (𝐺𝑘)) = (ω ↑o (𝐺𝑢)))
5856fveq2d 6542 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝐹‘(𝐺𝑘)) = (𝐹‘(𝐺𝑢)))
5957, 58oveq12d 7034 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
6054, 59syl5eq 2843 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑀 = ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))))
61 simpr 485 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝑓 = 𝑣)
6261dmeqd 5660 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → dom 𝑓 = dom 𝑣)
6362oveq1d 7031 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (dom 𝑓 +o 𝑦) = (dom 𝑣 +o 𝑦))
6460, 63mpteq12dv 5045 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦𝑀 ↦ (dom 𝑓 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
6553, 64syl5eq 2843 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) = (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)))
66 oveq2 7024 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑀 +o 𝑥) = (𝑀 +o 𝑦))
6766cbvmptv 5061 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦))
6860oveq1d 7031 . . . . . . . . . . . . . 14 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑀 +o 𝑦) = (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))
6962, 68mpteq12dv 5045 . . . . . . . . . . . . 13 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +o 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7067, 69syl5eq 2843 . . . . . . . . . . . 12 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7170cnveqd 5632 . . . . . . . . . . 11 ((𝑘 = 𝑢𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)))
7265, 71uneq12d 4061 . . . . . . . . . 10 ((𝑘 = 𝑢𝑓 = 𝑣) → ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7351, 72syl5eq 2843 . . . . . . . . 9 ((𝑘 = 𝑢𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))))
7447, 48, 49, 50, 73cbvmpo 7104 . . . . . . . 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 6542 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐺𝑢) = (𝐺𝐼))
7877oveq2d 7032 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (ω ↑o (𝐺𝑢)) = (ω ↑o (𝐺𝐼)))
7977fveq2d 6542 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝐼)))
8078, 79oveq12d 7034 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
81 simpr 485 . . . . . . . . . . . 12 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → 𝑣 = (𝑇𝐼))
8281dmeqd 5660 . . . . . . . . . . 11 ((𝑢 = 𝐼𝑣 = (𝑇𝐼)) → dom 𝑣 = dom (𝑇𝐼))
83 cnfcom.3 . . . . . . . . . . . 12 (𝜑 → (𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂)
84 f1odm 6487 . . . . . . . . . . . 12 ((𝑇𝐼):(𝐻𝐼)–1-1-onto𝑂 → dom (𝑇𝐼) = (𝐻𝐼))
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → dom (𝑇𝐼) = (𝐻𝐼))
8682, 85sylan9eqr 2853 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → dom 𝑣 = (𝐻𝐼))
8786oveq1d 7031 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (dom 𝑣 +o 𝑦) = ((𝐻𝐼) +o 𝑦))
8880, 87mpteq12dv 5045 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) = (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)))
8980oveq1d 7031 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))
9086, 89mpteq12dv 5045 . . . . . . . . 9 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9190cnveqd 5632 . . . . . . . 8 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦)) = (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)))
9288, 91uneq12d 4061 . . . . . . 7 ((𝜑 ∧ (𝑢 = 𝐼𝑣 = (𝑇𝐼))) → ((𝑦 ∈ ((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) ↦ (dom 𝑣 +o 𝑦)) ∪ (𝑦 ∈ dom 𝑣 ↦ (((ω ↑o (𝐺𝑢)) ·o (𝐹‘(𝐺𝑢))) +o 𝑦))) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
9318elexd 3457 . . . . . . 7 (𝜑𝐼 ∈ V)
94 fvexd 6553 . . . . . . 7 (𝜑 → (𝑇𝐼) ∈ V)
95 ovex 7048 . . . . . . . . . 10 ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ V
9695mptex 6852 . . . . . . . . 9 (𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∈ V
97 fvex 6551 . . . . . . . . . . 11 (𝐻𝐼) ∈ V
9897mptex 6852 . . . . . . . . . 10 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
9998cnvex 7486 . . . . . . . . 9 (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦)) ∈ V
10096, 99unex 7326 . . . . . . . 8 ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V
101100a1i 11 . . . . . . 7 (𝜑 → ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))) ∈ V)
10275, 92, 93, 94, 101ovmpod 7158 . . . . . 6 (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇𝐼)) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
10346, 102eqtrd 2831 . . . . 5 (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ↦ ((𝐻𝐼) +o 𝑦)) ∪ (𝑦 ∈ (𝐻𝐼) ↦ (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o 𝑦))))
104 f1oeq1 6472 . . . . 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 7026 . . . . . . . . . 10 (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)
111110a1i 11 . . . . . . . . 9 ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧))
112111mpoeq3ia 7090 . . . . . . . 8 (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧))
113 eqid 2795 . . . . . . . 8 ∅ = ∅
114 seqomeq12 7941 . . . . . . . 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 2819 . . . . . 6 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
1175, 107, 108, 19, 109, 116cantnfsuc 8979 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
1182, 13, 36, 117syl21anc 834 . . . 4 (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) +o (𝐻𝐼)))
119118f1oeq2d 6479 . . 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 6143 . . . . . 6 dom 𝐺 ⊆ suc dom 𝐺
122121, 18sseldi 3887 . . . . 5 (𝜑𝐼 ∈ suc dom 𝐺)
123 epelg 5354 . . . . . . . . . . 11 (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼𝑦𝐼))
12418, 123syl 17 . . . . . . . . . 10 (𝜑 → (𝑦 E 𝐼𝑦𝐼))
125124biimpar 478 . . . . . . . . 9 ((𝜑𝑦𝐼) → 𝑦 E 𝐼)
126 ovexd 7050 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ∈ V)
12733simpld 495 . . . . . . . . . . . 12 (𝜑 → E We (𝐹 supp ∅))
12819oiiso 8847 . . . . . . . . . . . 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 8839 . . . . . . . . . . . 12 Ord dom 𝐺
132 ordelss 6082 . . . . . . . . . . . 12 ((Ord dom 𝐺𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺)
133131, 18, 132sylancr 587 . . . . . . . . . . 11 (𝜑𝐼 ⊆ dom 𝐺)
134133sselda 3889 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝑦 ∈ dom 𝐺)
13518adantr 481 . . . . . . . . . 10 ((𝜑𝑦𝐼) → 𝐼 ∈ dom 𝐺)
136 isorel 6942 . . . . . . . . . 10 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
137130, 134, 135, 136syl12anc 833 . . . . . . . . 9 ((𝜑𝑦𝐼) → (𝑦 E 𝐼 ↔ (𝐺𝑦) E (𝐺𝐼)))
138125, 137mpbid 233 . . . . . . . 8 ((𝜑𝑦𝐼) → (𝐺𝑦) E (𝐺𝐼))
139 fvex 6551 . . . . . . . . 9 (𝐺𝐼) ∈ V
140139epeli 5356 . . . . . . . 8 ((𝐺𝑦) E (𝐺𝐼) ↔ (𝐺𝑦) ∈ (𝐺𝐼))
141138, 140sylib 219 . . . . . . 7 ((𝜑𝑦𝐼) → (𝐺𝑦) ∈ (𝐺𝐼))
142141ralrimiva 3149 . . . . . 6 (𝜑 → ∀𝑦𝐼 (𝐺𝑦) ∈ (𝐺𝐼))
143 ffun 6385 . . . . . . . 8 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺)
14420, 143ax-mp 5 . . . . . . 7 Fun 𝐺
145 funimass4 6598 . . . . . . 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 7457 . . . . . . 7 ∅ ∈ ω
152151a1i 11 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → ∅ ∈ ω)
153 simpr1 1187 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → 𝐼 ∈ suc dom 𝐺)
154 simpr2 1188 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐺𝐼) ∈ On)
155 simpr3 1189 . . . . . 6 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐺𝐼) ⊆ (𝐺𝐼))
1565, 148, 149, 19, 150, 116, 152, 153, 154, 155cantnflt 8981 . . . . 5 (((𝐴 ∈ On ∧ 𝐹𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺𝐼) ∈ On ∧ (𝐺𝐼) ⊆ (𝐺𝐼))) → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
1572, 13, 122, 25, 147, 156syl23anc 1370 . . . 4 (𝜑 → (𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)))
15816ffnd 6383 . . . . . . . . 9 (𝜑𝐹 Fn 𝐴)
159 0ex 5102 . . . . . . . . . 10 ∅ ∈ V
160159a1i 11 . . . . . . . . 9 (𝜑 → ∅ ∈ V)
161 elsuppfn 7689 . . . . . . . . 9 ((𝐹 Fn 𝐴𝐴 ∈ On ∧ ∅ ∈ V) → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
162158, 2, 160, 161syl3anc 1364 . . . . . . . 8 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅)))
163 simpr 485 . . . . . . . 8 (((𝐺𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺𝐼)) ≠ ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅)
164162, 163syl6bi 254 . . . . . . 7 (𝜑 → ((𝐺𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺𝐼)) ≠ ∅))
16522, 164mpd 15 . . . . . 6 (𝜑 → (𝐹‘(𝐺𝐼)) ≠ ∅)
166 on0eln0 6121 . . . . . . 7 ((𝐹‘(𝐺𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
16730, 166syl 17 . . . . . 6 (𝜑 → (∅ ∈ (𝐹‘(𝐺𝐼)) ↔ (𝐹‘(𝐺𝐼)) ≠ ∅))
168165, 167mpbird 258 . . . . 5 (𝜑 → ∅ ∈ (𝐹‘(𝐺𝐼)))
169 omword1 8049 . . . . 5 ((((ω ↑o (𝐺𝐼)) ∈ On ∧ (𝐹‘(𝐺𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺𝐼))) → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
17027, 30, 168, 169syl21anc 834 . . . 4 (𝜑 → (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
171 oaabs2 8122 . . . 4 ((((𝐻𝐼) ∈ (ω ↑o (𝐺𝐼)) ∧ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))) ∈ On) ∧ (ω ↑o (𝐺𝐼)) ⊆ ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
172157, 32, 170, 171syl21anc 834 . . 3 (𝜑 → ((𝐻𝐼) +o ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼)))) = ((ω ↑o (𝐺𝐼)) ·o (𝐹‘(𝐺𝐼))))
173172f1oeq3d 6480 . 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 1080   = wceq 1522  wcel 2081  wne 2984  wral 3105  Vcvv 3437  cun 3857  wss 3859  c0 4211   class class class wbr 4962  cmpt 5041   E cep 5352   We wwe 5401  ccnv 5442  dom cdm 5443  cima 5446  Ord word 6065  Oncon0 6066  suc csuc 6068  Fun wfun 6219   Fn wfn 6220  wf 6221  1-1-ontowf1o 6224  cfv 6225   Isom wiso 6226  (class class class)co 7016  cmpo 7018  ωcom 7436   supp csupp 7681  seq𝜔cseqom 7934   +o coa 7950   ·o comu 7951  o coe 7952   finSupp cfsupp 8679  OrdIsocoi 8819   CNF ccnf 8970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-supp 7682  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-seqom 7935  df-1o 7953  df-2o 7954  df-oadd 7957  df-omul 7958  df-oexp 7959  df-er 8139  df-map 8258  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-fsupp 8680  df-oi 8820  df-cnf 8971
This theorem is referenced by:  cnfcom  9009
  Copyright terms: Public domain W3C validator