ltrennb - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ltrennb		GIF version

Theorem ltrennb 7391

Description: Ordering of natural numbers with <_N or <_ℝ. (Contributed by Jim Kingdon, 13-Jul-2021.)

**Assertion**
Ref	Expression
ltrennb	⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <_N 𝐾 ↔ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R , 0_R⟩ <_ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R , 0_R⟩))

Distinct variable groups: 𝐽,𝑙 𝑢,𝐽 𝐾,𝑙 𝑢,𝐾

**Proof of Theorem ltrennb**
Step	Hyp	Ref	Expression
1		ltnnnq 6982	. . 3 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <_N 𝐾 ↔ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q [⟨𝐾, 1_𝑜⟩] ~_Q ))
2		nnnq 6981	. . . . 5 ⊢ (𝐽 ∈ N → [⟨𝐽, 1_𝑜⟩] ~_Q ∈ Q)
3	2	adantr 270	. . . 4 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → [⟨𝐽, 1_𝑜⟩] ~_Q ∈ Q)
4		nnnq 6981	. . . . 5 ⊢ (𝐾 ∈ N → [⟨𝐾, 1_𝑜⟩] ~_Q ∈ Q)
5	4	adantl 271	. . . 4 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → [⟨𝐾, 1_𝑜⟩] ~_Q ∈ Q)
6		ltnqpr 7152	. . . 4 ⊢ (([⟨𝐽, 1_𝑜⟩] ~_Q ∈ Q ∧ [⟨𝐾, 1_𝑜⟩] ~_Q ∈ Q) → ([⟨𝐽, 1_𝑜⟩] ~_Q <_Q [⟨𝐾, 1_𝑜⟩] ~_Q ↔ ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩<_P ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩))
7	3, 5, 6	syl2anc 403	. . 3 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → ([⟨𝐽, 1_𝑜⟩] ~_Q <_Q [⟨𝐾, 1_𝑜⟩] ~_Q ↔ ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩<_P ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩))
8		nqprlu 7106	. . . . 5 ⊢ ([⟨𝐽, 1_𝑜⟩] ~_Q ∈ Q → ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ∈ P)
9	3, 8	syl 14	. . . 4 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ∈ P)
10		nqprlu 7106	. . . . 5 ⊢ ([⟨𝐾, 1_𝑜⟩] ~_Q ∈ Q → ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ∈ P)
11	5, 10	syl 14	. . . 4 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ∈ P)
12		prsrlt 7332	. . . 4 ⊢ ((⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ∈ P ∧ ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ∈ P) → (⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩<_P ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ↔ [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R <_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ))
13	9, 11, 12	syl2anc 403	. . 3 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩<_P ⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ ↔ [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R <_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ))
14	1, 7, 13	3bitrd 212	. 2 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <_N 𝐾 ↔ [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R <_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ))
15		ltresr 7376	. 2 ⊢ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R , 0_R⟩ <_ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R , 0_R⟩ ↔ [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R <_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R )
16	14, 15	syl6bbr 196	1 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <_N 𝐾 ↔ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐽, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐽, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R , 0_R⟩ <_ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_Q [⟨𝐾, 1_𝑜⟩] ~_Q }, {𝑢 ∣ [⟨𝐾, 1_𝑜⟩] ~_Q <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R , 0_R⟩))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∈ wcel 1438 {cab 2074 ⟨cop 3449 class class class wbr 3845 (class class class)co 5652 1_𝑜c1o 6174 [cec 6290 Ncnpi 6831 <_N clti 6834 ~_Q ceq 6838 Qcnq 6839 <_Q cltq 6844 Pcnp 6850 1_Pc1p 6851 +_P cpp 6852 <_P cltp 6854 ~_R cer 6855 0_Rc0r 6857 <_R cltr 6862 <_ℝ 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: ltrenn 7392 axcaucvglemres 7434

W3C validator