![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > axpre-apti | GIF version |
Description: Apartness of reals is
tight. Axiom for real and complex numbers,
derived from set theory. This construction-dependent theorem should not
be referenced directly; instead, use ax-pre-apti 7460.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axpre-apti | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elreal 7366 | . . 3 ⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R 〈𝑥, 0R〉 = 𝐴) | |
2 | elreal 7366 | . . 3 ⊢ (𝐵 ∈ ℝ ↔ ∃𝑦 ∈ R 〈𝑦, 0R〉 = 𝐵) | |
3 | breq1 3848 | . . . . . 6 ⊢ (〈𝑥, 0R〉 = 𝐴 → (〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ↔ 𝐴 <ℝ 〈𝑦, 0R〉)) | |
4 | breq2 3849 | . . . . . 6 ⊢ (〈𝑥, 0R〉 = 𝐴 → (〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉 ↔ 〈𝑦, 0R〉 <ℝ 𝐴)) | |
5 | 3, 4 | orbi12d 742 | . . . . 5 ⊢ (〈𝑥, 0R〉 = 𝐴 → ((〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉) ↔ (𝐴 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 𝐴))) |
6 | 5 | notbid 627 | . . . 4 ⊢ (〈𝑥, 0R〉 = 𝐴 → (¬ (〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉) ↔ ¬ (𝐴 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 𝐴))) |
7 | eqeq1 2094 | . . . 4 ⊢ (〈𝑥, 0R〉 = 𝐴 → (〈𝑥, 0R〉 = 〈𝑦, 0R〉 ↔ 𝐴 = 〈𝑦, 0R〉)) | |
8 | 6, 7 | imbi12d 232 | . . 3 ⊢ (〈𝑥, 0R〉 = 𝐴 → ((¬ (〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉) → 〈𝑥, 0R〉 = 〈𝑦, 0R〉) ↔ (¬ (𝐴 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 𝐴) → 𝐴 = 〈𝑦, 0R〉))) |
9 | breq2 3849 | . . . . . 6 ⊢ (〈𝑦, 0R〉 = 𝐵 → (𝐴 <ℝ 〈𝑦, 0R〉 ↔ 𝐴 <ℝ 𝐵)) | |
10 | breq1 3848 | . . . . . 6 ⊢ (〈𝑦, 0R〉 = 𝐵 → (〈𝑦, 0R〉 <ℝ 𝐴 ↔ 𝐵 <ℝ 𝐴)) | |
11 | 9, 10 | orbi12d 742 | . . . . 5 ⊢ (〈𝑦, 0R〉 = 𝐵 → ((𝐴 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 𝐴) ↔ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) |
12 | 11 | notbid 627 | . . . 4 ⊢ (〈𝑦, 0R〉 = 𝐵 → (¬ (𝐴 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 𝐴) ↔ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) |
13 | eqeq2 2097 | . . . 4 ⊢ (〈𝑦, 0R〉 = 𝐵 → (𝐴 = 〈𝑦, 0R〉 ↔ 𝐴 = 𝐵)) | |
14 | 12, 13 | imbi12d 232 | . . 3 ⊢ (〈𝑦, 0R〉 = 𝐵 → ((¬ (𝐴 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 𝐴) → 𝐴 = 〈𝑦, 0R〉) ↔ (¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴) → 𝐴 = 𝐵))) |
15 | aptisr 7324 | . . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑦 ∈ R ∧ ¬ (𝑥 <R 𝑦 ∨ 𝑦 <R 𝑥)) → 𝑥 = 𝑦) | |
16 | 15 | 3expia 1145 | . . . 4 ⊢ ((𝑥 ∈ R ∧ 𝑦 ∈ R) → (¬ (𝑥 <R 𝑦 ∨ 𝑦 <R 𝑥) → 𝑥 = 𝑦)) |
17 | ltresr 7376 | . . . . . 6 ⊢ (〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ↔ 𝑥 <R 𝑦) | |
18 | ltresr 7376 | . . . . . 6 ⊢ (〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉 ↔ 𝑦 <R 𝑥) | |
19 | 17, 18 | orbi12i 716 | . . . . 5 ⊢ ((〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉) ↔ (𝑥 <R 𝑦 ∨ 𝑦 <R 𝑥)) |
20 | 19 | notbii 629 | . . . 4 ⊢ (¬ (〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉) ↔ ¬ (𝑥 <R 𝑦 ∨ 𝑦 <R 𝑥)) |
21 | vex 2622 | . . . . 5 ⊢ 𝑥 ∈ V | |
22 | 21 | eqresr 7373 | . . . 4 ⊢ (〈𝑥, 0R〉 = 〈𝑦, 0R〉 ↔ 𝑥 = 𝑦) |
23 | 16, 20, 22 | 3imtr4g 203 | . . 3 ⊢ ((𝑥 ∈ R ∧ 𝑦 ∈ R) → (¬ (〈𝑥, 0R〉 <ℝ 〈𝑦, 0R〉 ∨ 〈𝑦, 0R〉 <ℝ 〈𝑥, 0R〉) → 〈𝑥, 0R〉 = 〈𝑦, 0R〉)) |
24 | 1, 2, 8, 14, 23 | 2gencl 2652 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴) → 𝐴 = 𝐵)) |
25 | 24 | 3impia 1140 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 102 ∨ wo 664 ∧ w3a 924 = wceq 1289 ∈ wcel 1438 〈cop 3449 class class class wbr 3845 Rcnr 6856 0Rc0r 6857 <R cltr 6862 ℝcr 7349 <ℝ cltrr 7354 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 579 ax-in2 580 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-13 1449 ax-14 1450 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-coll 3954 ax-sep 3957 ax-nul 3965 ax-pow 4009 ax-pr 4036 ax-un 4260 ax-setind 4353 ax-iinf 4403 |
This theorem depends on definitions: df-bi 115 df-dc 781 df-3or 925 df-3an 926 df-tru 1292 df-fal 1295 df-nf 1395 df-sb 1693 df-eu 1951 df-mo 1952 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ne 2256 df-ral 2364 df-rex 2365 df-reu 2366 df-rab 2368 df-v 2621 df-sbc 2841 df-csb 2934 df-dif 3001 df-un 3003 df-in 3005 df-ss 3012 df-nul 3287 df-pw 3431 df-sn 3452 df-pr 3453 df-op 3455 df-uni 3654 df-int 3689 df-iun 3732 df-br 3846 df-opab 3900 df-mpt 3901 df-tr 3937 df-eprel 4116 df-id 4120 df-po 4123 df-iso 4124 df-iord 4193 df-on 4195 df-suc 4198 df-iom 4406 df-xp 4444 df-rel 4445 df-cnv 4446 df-co 4447 df-dm 4448 df-rn 4449 df-res 4450 df-ima 4451 df-iota 4980 df-fun 5017 df-fn 5018 df-f 5019 df-f1 5020 df-fo 5021 df-f1o 5022 df-fv 5023 df-ov 5655 df-oprab 5656 df-mpt2 5657 df-1st 5911 df-2nd 5912 df-recs 6070 df-irdg 6135 df-1o 6181 df-2o 6182 df-oadd 6185 df-omul 6186 df-er 6292 df-ec 6294 df-qs 6298 df-ni 6863 df-pli 6864 df-mi 6865 df-lti 6866 df-plpq 6903 df-mpq 6904 df-enq 6906 df-nqqs 6907 df-plqqs 6908 df-mqqs 6909 df-1nqqs 6910 df-rq 6911 df-ltnqqs 6912 df-enq0 6983 df-nq0 6984 df-0nq0 6985 df-plq0 6986 df-mq0 6987 df-inp 7025 df-i1p 7026 df-iplp 7027 df-iltp 7029 df-enr 7272 df-nr 7273 df-ltr 7276 df-0r 7277 df-r 7360 df-lt 7363 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |