Mathbox for ML < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cnfinltrel Structured version   Visualization version   GIF version

Theorem cnfinltrel 33578
 Description: Less than for the Cantor normal form is a relation. (Contributed by ML, 24-Jun-2022.)
Hypotheses
Ref Expression
cnfin.1 𝐼 = {⟨∅, 1𝑜⟩}
cnfin.add + = (𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑛 ∈ (dom 𝑦 ∪ dom 𝑧) ↦ ((𝑦𝑛) +𝑜 (𝑧𝑛))))
cnfin.tr (𝜑 ↔ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐))
cnfin.ltadd (𝜓 ↔ (𝑥 ∈ (dom 𝑐 ∪ ran 𝑐) ∧ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏)))
cnfin.ltexp (𝜒 ↔ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩})))
cnfin.yrule 𝑌 = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝑐 ∨ (𝜑 ∨ (𝜓𝜒)))}
cnfin.lt < = ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)
cnfin.def 𝐶 = dom <
Assertion
Ref Expression
cnfinltrel Rel <
Distinct variable groups:   𝐼,𝑐   𝑎,𝑏,𝑐,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑛,𝑎,𝑏,𝑐)   𝜓(𝑥,𝑦,𝑧,𝑛,𝑎,𝑏,𝑐)   𝜒(𝑥,𝑦,𝑧,𝑛,𝑎,𝑏,𝑐)   𝐶(𝑥,𝑦,𝑧,𝑛,𝑎,𝑏,𝑐)   + (𝑥,𝑦,𝑧,𝑛,𝑎,𝑏,𝑐)   < (𝑥,𝑦,𝑧,𝑛,𝑎,𝑏,𝑐)   𝐼(𝑥,𝑦,𝑧,𝑛,𝑎,𝑏)   𝑌(𝑥,𝑦,𝑧,𝑛,𝑎,𝑏,𝑐)

Proof of Theorem cnfinltrel
Dummy variables 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reluni 5380 . . 3 (Rel ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω) ↔ ∀𝑘 ∈ ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)Rel 𝑘)
2 frfnom 7683 . . . . 5 (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω) Fn ω
3 fvelrnb 6385 . . . . 5 ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω) Fn ω → (𝑘 ∈ ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω) ↔ ∃ ∈ ω ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = 𝑘))
42, 3ax-mp 5 . . . 4 (𝑘 ∈ ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω) ↔ ∃ ∈ ω ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = 𝑘)
5 0ex 4924 . . . . . . . . 9 ∅ ∈ V
6 cnfin.1 . . . . . . . . . 10 𝐼 = {⟨∅, 1𝑜⟩}
7 snex 5036 . . . . . . . . . 10 {⟨∅, 1𝑜⟩} ∈ V
86, 7eqeltri 2846 . . . . . . . . 9 𝐼 ∈ V
95, 8relsnop 5367 . . . . . . . 8 Rel {⟨∅, 𝐼⟩}
10 fveq2 6332 . . . . . . . . . . 11 ( = ∅ → ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘∅))
11 snex 5036 . . . . . . . . . . . 12 {⟨∅, 𝐼⟩} ∈ V
12 fr0g 7684 . . . . . . . . . . . 12 ({⟨∅, 𝐼⟩} ∈ V → ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘∅) = {⟨∅, 𝐼⟩})
1311, 12ax-mp 5 . . . . . . . . . . 11 ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘∅) = {⟨∅, 𝐼⟩}
1410, 13syl6eq 2821 . . . . . . . . . 10 ( = ∅ → ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = {⟨∅, 𝐼⟩})
1514releqd 5343 . . . . . . . . 9 ( = ∅ → (Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ↔ Rel {⟨∅, 𝐼⟩}))
165, 15sbcie 3622 . . . . . . . 8 ([∅ / ]Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ↔ Rel {⟨∅, 𝐼⟩})
179, 16mpbir 221 . . . . . . 7 [∅ / ]Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘)
18 fvex 6342 . . . . . . . . . . . 12 ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ∈ V
19 cnfin.yrule . . . . . . . . . . . . . 14 𝑌 = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝑐 ∨ (𝜑 ∨ (𝜓𝜒)))}
2019relopabi 5384 . . . . . . . . . . . . 13 Rel 𝑌
2120sbcth 3602 . . . . . . . . . . . 12 (((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ∈ V → [((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐]Rel 𝑌)
2218, 21ax-mp 5 . . . . . . . . . . 11 [((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐]Rel 𝑌
23 sbcrel 5345 . . . . . . . . . . . 12 (((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ∈ V → ([((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐]Rel 𝑌 ↔ Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌))
2418, 23ax-mp 5 . . . . . . . . . . 11 ([((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐]Rel 𝑌 ↔ Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌)
2522, 24mpbi 220 . . . . . . . . . 10 Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌
26 frsuc 7685 . . . . . . . . . . . 12 ( ∈ ω → ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘suc ) = ((𝑐 ∈ V ↦ 𝑌)‘((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘)))
27 cnfin.ltexp . . . . . . . . . . . . . . . . 17 (𝜒 ↔ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩})))
2827opabbii 4851 . . . . . . . . . . . . . . . 16 {⟨𝑥, 𝑦⟩ ∣ 𝜒} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))}
29 vex 3354 . . . . . . . . . . . . . . . . . . 19 𝑐 ∈ V
3029dmex 7246 . . . . . . . . . . . . . . . . . 18 dom 𝑐 ∈ V
3129rnex 7247 . . . . . . . . . . . . . . . . . 18 ran 𝑐 ∈ V
3230, 31ab2rexex 7306 . . . . . . . . . . . . . . . . 17 {𝑧 ∣ ∃𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩} ∈ V
33 df-opab 4847 . . . . . . . . . . . . . . . . . 18 {⟨𝑥, 𝑦⟩ ∣ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩})))}
34 19.42vv 2035 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎𝑏(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))))
35342exbii 1925 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑥𝑦𝑎𝑏(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))))
36 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
37 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏 ∈ V
3836, 37opeldm 5466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑎, 𝑏⟩ ∈ 𝑐𝑎 ∈ dom 𝑐)
3936, 37opelrn 5495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑎, 𝑏⟩ ∈ 𝑐𝑏 ∈ ran 𝑐)
4038, 39jca 501 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑎, 𝑏⟩ ∈ 𝑐 → (𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐))
4140ad2antrl 707 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) → (𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐))
42 opeq12 4541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}) → ⟨𝑥, 𝑦⟩ = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩)
4342eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}) → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩))
4443biimpac 464 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩})) → 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩)
4544adantrl 695 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) → 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩)
4641, 45jca 501 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) → ((𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐) ∧ 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩))
47462eximi 1911 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎𝑏(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) → ∃𝑎𝑏((𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐) ∧ 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩))
4847exlimivv 2012 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑥𝑦𝑎𝑏(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) → ∃𝑎𝑏((𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐) ∧ 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩))
4935, 48sylbir 225 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) → ∃𝑎𝑏((𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐) ∧ 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩))
50 r2ex 3209 . . . . . . . . . . . . . . . . . . . 20 (∃𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩ ↔ ∃𝑎𝑏((𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐) ∧ 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩))
5149, 50sylibr 224 . . . . . . . . . . . . . . . . . . 19 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))) → ∃𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩)
5251ss2abi 3823 . . . . . . . . . . . . . . . . . 18 {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩})))} ⊆ {𝑧 ∣ ∃𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩}
5333, 52eqsstri 3784 . . . . . . . . . . . . . . . . 17 {⟨𝑥, 𝑦⟩ ∣ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))} ⊆ {𝑧 ∣ ∃𝑎 ∈ dom 𝑐𝑏 ∈ ran 𝑐 𝑧 = ⟨{⟨𝑎, 1𝑜⟩}, {⟨𝑏, 1𝑜⟩}⟩}
5432, 53ssexi 4937 . . . . . . . . . . . . . . . 16 {⟨𝑥, 𝑦⟩ ∣ ∃𝑎𝑏(⟨𝑎, 𝑏⟩ ∈ 𝑐 ∧ (𝑥 = {⟨𝑎, 1𝑜⟩} ∧ 𝑦 = {⟨𝑏, 1𝑜⟩}))} ∈ V
5528, 54eqeltri 2846 . . . . . . . . . . . . . . 15 {⟨𝑥, 𝑦⟩ ∣ 𝜒} ∈ V
56 unopab 4862 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜒}) = {⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)}
57 cnfin.ltadd . . . . . . . . . . . . . . . . . . . 20 (𝜓 ↔ (𝑥 ∈ (dom 𝑐 ∪ ran 𝑐) ∧ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏)))
5857opabbii 4851 . . . . . . . . . . . . . . . . . . 19 {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (dom 𝑐 ∪ ran 𝑐) ∧ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏))}
5930, 31unex 7103 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑐 ∪ ran 𝑐) ∈ V
60 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦ran 𝑐
61 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑦𝑥
62 cnfin.add . . . . . . . . . . . . . . . . . . . . . . . . . . 27 + = (𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑛 ∈ (dom 𝑦 ∪ dom 𝑧) ↦ ((𝑦𝑛) +𝑜 (𝑧𝑛))))
63 nfmpt21 6869 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑦(𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑛 ∈ (dom 𝑦 ∪ dom 𝑧) ↦ ((𝑦𝑛) +𝑜 (𝑧𝑛))))
6462, 63nfcxfr 2911 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑦 +
65 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑦𝑏
6661, 64, 65nfov 6821 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦(𝑥 + 𝑏)
6766nfeq2 2929 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 𝑘 = (𝑥 + 𝑏)
6860, 67nfrex 3155 . . . . . . . . . . . . . . . . . . . . . . 23 𝑦𝑏 ∈ ran 𝑐 𝑘 = (𝑥 + 𝑏)
69 nfv 1995 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏)
70 eqeq1 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑦 → (𝑘 = (𝑥 + 𝑏) ↔ 𝑦 = (𝑥 + 𝑏)))
7170rexbidv 3200 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑦 → (∃𝑏 ∈ ran 𝑐 𝑘 = (𝑥 + 𝑏) ↔ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏)))
7268, 69, 71cbvab 2895 . . . . . . . . . . . . . . . . . . . . . 22 {𝑘 ∣ ∃𝑏 ∈ ran 𝑐 𝑘 = (𝑥 + 𝑏)} = {𝑦 ∣ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏)}
73 abrexexg 7287 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑐 ∈ V → {𝑘 ∣ ∃𝑏 ∈ ran 𝑐 𝑘 = (𝑥 + 𝑏)} ∈ V)
7431, 73ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 {𝑘 ∣ ∃𝑏 ∈ ran 𝑐 𝑘 = (𝑥 + 𝑏)} ∈ V
7572, 74eqeltrri 2847 . . . . . . . . . . . . . . . . . . . . 21 {𝑦 ∣ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏)} ∈ V
7675a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (dom 𝑐 ∪ ran 𝑐) → {𝑦 ∣ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏)} ∈ V)
7759, 76opabex3 7293 . . . . . . . . . . . . . . . . . . 19 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (dom 𝑐 ∪ ran 𝑐) ∧ ∃𝑏 ∈ ran 𝑐 𝑦 = (𝑥 + 𝑏))} ∈ V
7858, 77eqeltri 2846 . . . . . . . . . . . . . . . . . 18 {⟨𝑥, 𝑦⟩ ∣ 𝜓} ∈ V
79 unexg 7106 . . . . . . . . . . . . . . . . . 18 (({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∈ V ∧ {⟨𝑥, 𝑦⟩ ∣ 𝜒} ∈ V) → ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜒}) ∈ V)
8078, 79mpan 670 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩ ∣ 𝜒} ∈ V → ({⟨𝑥, 𝑦⟩ ∣ 𝜓} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜒}) ∈ V)
8156, 80syl5eqelr 2855 . . . . . . . . . . . . . . . 16 ({⟨𝑥, 𝑦⟩ ∣ 𝜒} ∈ V → {⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)} ∈ V)
82 unopab 4862 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))}
83 cnfin.tr . . . . . . . . . . . . . . . . . . . 20 (𝜑 ↔ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐))
8483opabbii 4851 . . . . . . . . . . . . . . . . . . 19 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐)}
8530, 31xpex 7109 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑐 × ran 𝑐) ∈ V
86 df-opab 4847 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐)} = {𝑙 ∣ ∃𝑥𝑦(𝑙 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐))}
87 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = ⟨𝑥, 𝑦⟩ → (𝑙 ∈ (dom 𝑐 × ran 𝑐) ↔ ⟨𝑥, 𝑦⟩ ∈ (dom 𝑐 × ran 𝑐)))
8887biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = ⟨𝑥, 𝑦⟩ → (⟨𝑥, 𝑦⟩ ∈ (dom 𝑐 × ran 𝑐) → 𝑙 ∈ (dom 𝑐 × ran 𝑐)))
89 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
90 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 ∈ V
9189, 90opeldm 5466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑥, 𝑧⟩ ∈ 𝑐𝑥 ∈ dom 𝑐)
92 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑦 ∈ V
9390, 92opelrn 5495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑧, 𝑦⟩ ∈ 𝑐𝑦 ∈ ran 𝑐)
94 opelxpi 5288 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ dom 𝑐𝑦 ∈ ran 𝑐) → ⟨𝑥, 𝑦⟩ ∈ (dom 𝑐 × ran 𝑐))
9591, 93, 94syl2an 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐) → ⟨𝑥, 𝑦⟩ ∈ (dom 𝑐 × ran 𝑐))
9695exlimiv 2010 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐) → ⟨𝑥, 𝑦⟩ ∈ (dom 𝑐 × ran 𝑐))
9788, 96impel 495 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐)) → 𝑙 ∈ (dom 𝑐 × ran 𝑐))
9897exlimivv 2012 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥𝑦(𝑙 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐)) → 𝑙 ∈ (dom 𝑐 × ran 𝑐))
9998abssi 3826 . . . . . . . . . . . . . . . . . . . . 21 {𝑙 ∣ ∃𝑥𝑦(𝑙 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐))} ⊆ (dom 𝑐 × ran 𝑐)
10086, 99eqsstri 3784 . . . . . . . . . . . . . . . . . . . 20 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐)} ⊆ (dom 𝑐 × ran 𝑐)
10185, 100ssexi 4937 . . . . . . . . . . . . . . . . . . 19 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑐 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝑐)} ∈ V
10284, 101eqeltri 2846 . . . . . . . . . . . . . . . . . 18 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∈ V
103 unexg 7106 . . . . . . . . . . . . . . . . . 18 (({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∈ V ∧ {⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)} ∈ V) → ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)}) ∈ V)
104102, 103mpan 670 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)} ∈ V → ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)}) ∈ V)
10582, 104syl5eqelr 2855 . . . . . . . . . . . . . . . 16 ({⟨𝑥, 𝑦⟩ ∣ (𝜓𝜒)} ∈ V → {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))} ∈ V)
106 unopab 4862 . . . . . . . . . . . . . . . . . 18 ({⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))}) = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝑐 ∨ (𝜑 ∨ (𝜓𝜒)))}
107106, 19eqtr4i 2796 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))}) = 𝑌
108 df-opab 4847 . . . . . . . . . . . . . . . . . . . 20 {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} = {𝑙 ∣ ∃𝑥𝑦(𝑙 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑐)}
109 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = ⟨𝑥, 𝑦⟩ → (𝑙𝑐 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑐))
110109biimprd 238 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = ⟨𝑥, 𝑦⟩ → (⟨𝑥, 𝑦⟩ ∈ 𝑐𝑙𝑐))
111 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑥, 𝑦⟩ ∈ 𝑐 → ⟨𝑥, 𝑦⟩ ∈ 𝑐)
112110, 111impel 495 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑙 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑐) → 𝑙𝑐)
113112exlimivv 2012 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑥𝑦(𝑙 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑐) → 𝑙𝑐)
114113abssi 3826 . . . . . . . . . . . . . . . . . . . 20 {𝑙 ∣ ∃𝑥𝑦(𝑙 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑐)} ⊆ 𝑐
115108, 114eqsstri 3784 . . . . . . . . . . . . . . . . . . 19 {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} ⊆ 𝑐
11629, 115ssexi 4937 . . . . . . . . . . . . . . . . . 18 {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} ∈ V
117 unexg 7106 . . . . . . . . . . . . . . . . . 18 (({⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} ∈ V ∧ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))} ∈ V) → ({⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))}) ∈ V)
118116, 117mpan 670 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))} ∈ V → ({⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝑐} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))}) ∈ V)
119107, 118syl5eqelr 2855 . . . . . . . . . . . . . . . 16 ({⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ (𝜓𝜒))} ∈ V → 𝑌 ∈ V)
12081, 105, 1193syl 18 . . . . . . . . . . . . . . 15 ({⟨𝑥, 𝑦⟩ ∣ 𝜒} ∈ V → 𝑌 ∈ V)
12155, 120ax-mp 5 . . . . . . . . . . . . . 14 𝑌 ∈ V
122121csbex 4927 . . . . . . . . . . . . 13 ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌 ∈ V
123 eqid 2771 . . . . . . . . . . . . . 14 (𝑐 ∈ V ↦ 𝑌) = (𝑐 ∈ V ↦ 𝑌)
124123fvmpts 6427 . . . . . . . . . . . . 13 ((((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ∈ V ∧ ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌 ∈ V) → ((𝑐 ∈ V ↦ 𝑌)‘((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘)) = ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌)
12518, 122, 124mp2an 672 . . . . . . . . . . . 12 ((𝑐 ∈ V ↦ 𝑌)‘((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘)) = ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌
12626, 125syl6eq 2821 . . . . . . . . . . 11 ( ∈ ω → ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘suc ) = ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌)
127126releqd 5343 . . . . . . . . . 10 ( ∈ ω → (Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘suc ) ↔ Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) / 𝑐𝑌))
12825, 127mpbiri 248 . . . . . . . . 9 ( ∈ ω → Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘suc ))
129 vex 3354 . . . . . . . . . . . 12 ∈ V
130129sucex 7158 . . . . . . . . . . 11 suc ∈ V
131 sbcrel 5345 . . . . . . . . . . 11 (suc ∈ V → ([suc / ]Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ↔ Rel suc / ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘)))
132130, 131ax-mp 5 . . . . . . . . . 10 ([suc / ]Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ↔ Rel suc / ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘))
133 csbfv 6374 . . . . . . . . . . 11 suc / ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘suc )
134133releqi 5342 . . . . . . . . . 10 (Rel suc / ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ↔ Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘suc ))
135132, 134bitri 264 . . . . . . . . 9 ([suc / ]Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ↔ Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘suc ))
136128, 135sylibr 224 . . . . . . . 8 ( ∈ ω → [suc / ]Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘))
137136a1d 25 . . . . . . 7 ( ∈ ω → (Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) → [suc / ]Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘)))
13817, 137findes 7243 . . . . . 6 ( ∈ ω → Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘))
139 releq 5341 . . . . . 6 (((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = 𝑘 → (Rel ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) ↔ Rel 𝑘))
140138, 139syl5ibcom 235 . . . . 5 ( ∈ ω → (((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = 𝑘 → Rel 𝑘))
141140rexlimiv 3175 . . . 4 (∃ ∈ ω ((rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)‘) = 𝑘 → Rel 𝑘)
1424, 141sylbi 207 . . 3 (𝑘 ∈ ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω) → Rel 𝑘)
1431, 142mprgbir 3076 . 2 Rel ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)
144 cnfin.lt . . 3 < = ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω)
145144releqi 5342 . 2 (Rel < ↔ Rel ran (rec((𝑐 ∈ V ↦ 𝑌), {⟨∅, 𝐼⟩}) ↾ ω))
146143, 145mpbir 221 1 Rel <
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 382   ∨ wo 836   = wceq 1631  ∃wex 1852   ∈ wcel 2145  {cab 2757  ∃wrex 3062  Vcvv 3351  [wsbc 3587  ⦋csb 3682   ∪ cun 3721  ∅c0 4063  {csn 4316  ⟨cop 4322  ∪ cuni 4574  {copab 4846   ↦ cmpt 4863   × cxp 5247  dom cdm 5249  ran crn 5250   ↾ cres 5251  Rel wrel 5254  suc csuc 5868   Fn wfn 6026  ‘cfv 6031  (class class class)co 6793   ↦ cmpt2 6795  ωcom 7212  reccrdg 7658  1𝑜c1o 7706   +𝑜 coa 7710 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator