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

Theorem ordtbaslem 20709
Description: Lemma for ordtbas 20713. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.)
Hypotheses
Ref Expression
ordtval.1 𝑋 = dom 𝑅
ordtval.2 𝐴 = ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
Assertion
Ref Expression
ordtbaslem (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)

Proof of Theorem ordtbaslem
Dummy variables 𝑎 𝑏 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3anrot 1035 . . . . . . . . . . . . 13 ((𝑦𝑋𝑎𝑋𝑏𝑋) ↔ (𝑎𝑋𝑏𝑋𝑦𝑋))
2 ordtval.1 . . . . . . . . . . . . . 14 𝑋 = dom 𝑅
32tsrlemax 16939 . . . . . . . . . . . . 13 ((𝑅 ∈ TosetRel ∧ (𝑦𝑋𝑎𝑋𝑏𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
41, 3sylan2br 491 . . . . . . . . . . . 12 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋𝑦𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
543exp2 1276 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → (𝑎𝑋 → (𝑏𝑋 → (𝑦𝑋 → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏))))))
65imp42 617 . . . . . . . . . 10 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
76notbid 306 . . . . . . . . 9 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ ¬ (𝑦𝑅𝑎𝑦𝑅𝑏)))
8 ioran 509 . . . . . . . . 9 (¬ (𝑦𝑅𝑎𝑦𝑅𝑏) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏))
97, 8syl6bb 274 . . . . . . . 8 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)))
109rabbidva 3067 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
11 ifcl 3983 . . . . . . . . . 10 ((𝑏𝑋𝑎𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
1211ancoms 467 . . . . . . . . 9 ((𝑎𝑋𝑏𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
1312adantl 480 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
14 dmexg 6863 . . . . . . . . . . . 12 (𝑅 ∈ TosetRel → dom 𝑅 ∈ V)
152, 14syl5eqel 2596 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → 𝑋 ∈ V)
1615adantr 479 . . . . . . . . . 10 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → 𝑋 ∈ V)
17 rabexg 4638 . . . . . . . . . 10 (𝑋 ∈ V → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1816, 17syl 17 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1910, 18eqeltrd 2592 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V)
20 eqid 2514 . . . . . . . . . 10 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
21 breq2 4485 . . . . . . . . . . . 12 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (𝑦𝑅𝑥𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2221notbid 306 . . . . . . . . . . 11 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2322rabbidv 3068 . . . . . . . . . 10 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)})
2420, 23elrnmpt1s 5185 . . . . . . . . 9 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}))
25 ordtval.2 . . . . . . . . 9 𝐴 = ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
2624, 25syl6eleqr 2603 . . . . . . . 8 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2713, 19, 26syl2anc 690 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2810, 27eqeltrrd 2593 . . . . . 6 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
2928ralrimivva 2858 . . . . 5 (𝑅 ∈ TosetRel → ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
30 rabexg 4638 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3115, 30syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3231ralrimivw 2854 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
33 breq2 4485 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑦𝑅𝑥𝑦𝑅𝑎))
3433notbid 306 . . . . . . . . 9 (𝑥 = 𝑎 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑎))
3534rabbidv 3068 . . . . . . . 8 (𝑥 = 𝑎 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
3635cbvmptv 4576 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑎𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
37 ineq1 3672 . . . . . . . . . 10 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
38 inrab 3761 . . . . . . . . . 10 ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)}
3937, 38syl6eq 2564 . . . . . . . . 9 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
4039eleq1d 2576 . . . . . . . 8 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → ((𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4140ralbidv 2873 . . . . . . 7 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4236, 41ralrnmpt 6159 . . . . . 6 (∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4332, 42syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4429, 43mpbird 245 . . . 4 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)
45 rabexg 4638 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4615, 45syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4746ralrimivw 2854 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
48 breq2 4485 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑦𝑅𝑥𝑦𝑅𝑏))
4948notbid 306 . . . . . . . . 9 (𝑥 = 𝑏 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑏))
5049rabbidv 3068 . . . . . . . 8 (𝑥 = 𝑏 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
5150cbvmptv 4576 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑏𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
52 ineq2 3673 . . . . . . . 8 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → (𝑧𝑤) = (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
5352eleq1d 2576 . . . . . . 7 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → ((𝑧𝑤) ∈ 𝐴 ↔ (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5451, 53ralrnmpt 6159 . . . . . 6 (∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5547, 54syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5655ralbidv 2873 . . . 4 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5744, 56mpbird 245 . . 3 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5825raleqi 3023 . . . 4 (∀𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5925, 58raleqbii 2877 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
6057, 59sylibr 222 . 2 (𝑅 ∈ TosetRel → ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
61 pwexg 4675 . . . . 5 (𝑋 ∈ V → 𝒫 𝑋 ∈ V)
6215, 61syl 17 . . . 4 (𝑅 ∈ TosetRel → 𝒫 𝑋 ∈ V)
63 ssrab2 3554 . . . . . . . 8 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋
6415adantr 479 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → 𝑋 ∈ V)
65 elpw2g 4653 . . . . . . . . 9 (𝑋 ∈ V → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6664, 65syl 17 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6763, 66mpbiri 246 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋)
6867, 20fmptd 6175 . . . . . 6 (𝑅 ∈ TosetRel → (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋)
69 frn 5851 . . . . . 6 ((𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋 → ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋)
7068, 69syl 17 . . . . 5 (𝑅 ∈ TosetRel → ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋)
7125, 70syl5eqss 3516 . . . 4 (𝑅 ∈ TosetRel → 𝐴 ⊆ 𝒫 𝑋)
7262, 71ssexd 4632 . . 3 (𝑅 ∈ TosetRel → 𝐴 ∈ V)
73 inficl 8088 . . 3 (𝐴 ∈ V → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7472, 73syl 17 . 2 (𝑅 ∈ TosetRel → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7560, 74mpbid 220 1 (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1938  wral 2800  {crab 2804  Vcvv 3077  cin 3443  wss 3444  ifcif 3939  𝒫 cpw 4011   class class class wbr 4481  cmpt 4541  dom cdm 4932  ran crn 4933  wf 5685  cfv 5689  ficfi 8073   TosetRel ctsr 16918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-reu 2807  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-om 6832  df-wrecs 7167  df-recs 7229  df-rdg 7267  df-1o 7321  df-oadd 7325  df-er 7503  df-en 7716  df-fin 7719  df-fi 8074  df-ps 16919  df-tsr 16920
This theorem is referenced by:  ordtbas2  20712
  Copyright terms: Public domain W3C validator