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

Theorem ordtbaslem 21404
 Description: Lemma for ordtbas 21408. 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 1085 . . . . . . . . . . . . 13 ((𝑦𝑋𝑎𝑋𝑏𝑋) ↔ (𝑎𝑋𝑏𝑋𝑦𝑋))
2 ordtval.1 . . . . . . . . . . . . . 14 𝑋 = dom 𝑅
32tsrlemax 17610 . . . . . . . . . . . . 13 ((𝑅 ∈ TosetRel ∧ (𝑦𝑋𝑎𝑋𝑏𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
41, 3sylan2br 588 . . . . . . . . . . . 12 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋𝑦𝑋)) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
543exp2 1416 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → (𝑎𝑋 → (𝑏𝑋 → (𝑦𝑋 → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏))))))
65imp42 419 . . . . . . . . . 10 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (𝑦𝑅𝑎𝑦𝑅𝑏)))
76notbid 310 . . . . . . . . 9 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ ¬ (𝑦𝑅𝑎𝑦𝑅𝑏)))
8 ioran 969 . . . . . . . . 9 (¬ (𝑦𝑅𝑎𝑦𝑅𝑏) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏))
97, 8syl6bb 279 . . . . . . . 8 (((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) ∧ 𝑦𝑋) → (¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎) ↔ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)))
109rabbidva 3385 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
11 ifcl 4351 . . . . . . . . . 10 ((𝑏𝑋𝑎𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
1211ancoms 452 . . . . . . . . 9 ((𝑎𝑋𝑏𝑋) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
1312adantl 475 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋)
14 dmexg 7377 . . . . . . . . . . . 12 (𝑅 ∈ TosetRel → dom 𝑅 ∈ V)
152, 14syl5eqel 2863 . . . . . . . . . . 11 (𝑅 ∈ TosetRel → 𝑋 ∈ V)
1615adantr 474 . . . . . . . . . 10 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → 𝑋 ∈ V)
17 rabexg 5050 . . . . . . . . . 10 (𝑋 ∈ V → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1816, 17syl 17 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ V)
1910, 18eqeltrd 2859 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V)
20 eqid 2778 . . . . . . . . . 10 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
21 breq2 4892 . . . . . . . . . . . 12 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (𝑦𝑅𝑥𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2221notbid 310 . . . . . . . . . . 11 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)))
2322rabbidv 3386 . . . . . . . . . 10 (𝑥 = if(𝑎𝑅𝑏, 𝑏, 𝑎) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)})
2420, 23elrnmpt1s 5621 . . . . . . . . 9 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}))
25 ordtval.2 . . . . . . . . 9 𝐴 = ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})
2624, 25syl6eleqr 2870 . . . . . . . 8 ((if(𝑎𝑅𝑏, 𝑏, 𝑎) ∈ 𝑋 ∧ {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ V) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2713, 19, 26syl2anc 579 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ ¬ 𝑦𝑅if(𝑎𝑅𝑏, 𝑏, 𝑎)} ∈ 𝐴)
2810, 27eqeltrrd 2860 . . . . . 6 ((𝑅 ∈ TosetRel ∧ (𝑎𝑋𝑏𝑋)) → {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
2928ralrimivva 3153 . . . . 5 (𝑅 ∈ TosetRel → ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴)
30 rabexg 5050 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3115, 30syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
3231ralrimivw 3149 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
33 breq2 4892 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑦𝑅𝑥𝑦𝑅𝑎))
3433notbid 310 . . . . . . . . 9 (𝑥 = 𝑎 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑎))
3534rabbidv 3386 . . . . . . . 8 (𝑥 = 𝑎 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
3635cbvmptv 4987 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑎𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎})
37 ineq1 4030 . . . . . . . . . 10 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
38 inrab 4125 . . . . . . . . . 10 ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)}
3937, 38syl6eq 2830 . . . . . . . . 9 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) = {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)})
4039eleq1d 2844 . . . . . . . 8 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → ((𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4140ralbidv 3168 . . . . . . 7 (𝑧 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} → (∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4236, 41ralrnmpt 6634 . . . . . 6 (∀𝑎𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4332, 42syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴 ↔ ∀𝑎𝑋𝑏𝑋 {𝑦𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑦𝑅𝑏)} ∈ 𝐴))
4429, 43mpbird 249 . . . 4 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴)
45 rabexg 5050 . . . . . . . 8 (𝑋 ∈ V → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4615, 45syl 17 . . . . . . 7 (𝑅 ∈ TosetRel → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
4746ralrimivw 3149 . . . . . 6 (𝑅 ∈ TosetRel → ∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V)
48 breq2 4892 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑦𝑅𝑥𝑦𝑅𝑏))
4948notbid 310 . . . . . . . . 9 (𝑥 = 𝑏 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑏))
5049rabbidv 3386 . . . . . . . 8 (𝑥 = 𝑏 → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
5150cbvmptv 4987 . . . . . . 7 (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑏𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏})
52 ineq2 4031 . . . . . . . 8 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → (𝑧𝑤) = (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}))
5352eleq1d 2844 . . . . . . 7 (𝑤 = {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} → ((𝑧𝑤) ∈ 𝐴 ↔ (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5451, 53ralrnmpt 6634 . . . . . 6 (∀𝑏𝑋 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏} ∈ V → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5547, 54syl 17 . . . . 5 (𝑅 ∈ TosetRel → (∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5655ralbidv 3168 . . . 4 (𝑅 ∈ TosetRel → (∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑏𝑋 (𝑧 ∩ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑏}) ∈ 𝐴))
5744, 56mpbird 249 . . 3 (𝑅 ∈ TosetRel → ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5825raleqi 3338 . . . 4 (∀𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
5925, 58raleqbii 3172 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ ∀𝑧 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})∀𝑤 ∈ ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥})(𝑧𝑤) ∈ 𝐴)
6057, 59sylibr 226 . 2 (𝑅 ∈ TosetRel → ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
6115pwexd 5093 . . . 4 (𝑅 ∈ TosetRel → 𝒫 𝑋 ∈ V)
62 ssrab2 3908 . . . . . . . 8 {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋
6315adantr 474 . . . . . . . . 9 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → 𝑋 ∈ V)
64 elpw2g 5063 . . . . . . . . 9 (𝑋 ∈ V → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6563, 64syl 17 . . . . . . . 8 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → ({𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋))
6662, 65mpbiri 250 . . . . . . 7 ((𝑅 ∈ TosetRel ∧ 𝑥𝑋) → {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋)
6766fmpttd 6651 . . . . . 6 (𝑅 ∈ TosetRel → (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋)
6867frnd 6300 . . . . 5 (𝑅 ∈ TosetRel → ran (𝑥𝑋 ↦ {𝑦𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋)
6925, 68syl5eqss 3868 . . . 4 (𝑅 ∈ TosetRel → 𝐴 ⊆ 𝒫 𝑋)
7061, 69ssexd 5044 . . 3 (𝑅 ∈ TosetRel → 𝐴 ∈ V)
71 inficl 8621 . . 3 (𝐴 ∈ V → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7270, 71syl 17 . 2 (𝑅 ∈ TosetRel → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
7360, 72mpbid 224 1 (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107  ∀wral 3090  {crab 3094  Vcvv 3398   ∩ cin 3791   ⊆ wss 3792  ifcif 4307  𝒫 cpw 4379   class class class wbr 4888   ↦ cmpt 4967  dom cdm 5357  ran crn 5358  ‘cfv 6137  ficfi 8606   TosetRel ctsr 17589 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-en 8244  df-fin 8247  df-fi 8607  df-ps 17590  df-tsr 17591 This theorem is referenced by:  ordtbas2  21407
 Copyright terms: Public domain W3C validator