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

Theorem pitonnlem1 6921
 Description: Lemma for pitonn 6924. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.)
Assertion
Ref Expression
pitonnlem1 ⟨[⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 1
Distinct variable group:   𝑢,𝑙

Proof of Theorem pitonnlem1
StepHypRef Expression
1 df-1 6897 . 2 1 = ⟨1R, 0R
2 df-1r 6817 . . . 4 1R = [⟨(1P +P 1P), 1P⟩] ~R
3 df-i1p 6565 . . . . . . . 8 1P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
4 df-1nqqs 6449 . . . . . . . . . . 11 1Q = [⟨1𝑜, 1𝑜⟩] ~Q
54breq2i 3772 . . . . . . . . . 10 (𝑙 <Q 1Q𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q )
65abbii 2153 . . . . . . . . 9 {𝑙𝑙 <Q 1Q} = {𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }
74breq1i 3771 . . . . . . . . . 10 (1Q <Q 𝑢 ↔ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢)
87abbii 2153 . . . . . . . . 9 {𝑢 ∣ 1Q <Q 𝑢} = {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}
96, 8opeq12i 3554 . . . . . . . 8 ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩
103, 9eqtri 2060 . . . . . . 7 1P = ⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩
1110oveq1i 5522 . . . . . 6 (1P +P 1P) = (⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)
1211opeq1i 3552 . . . . 5 ⟨(1P +P 1P), 1P⟩ = ⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P
13 eceq1 6141 . . . . 5 (⟨(1P +P 1P), 1P⟩ = ⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ → [⟨(1P +P 1P), 1P⟩] ~R = [⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
1412, 13ax-mp 7 . . . 4 [⟨(1P +P 1P), 1P⟩] ~R = [⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R
152, 14eqtri 2060 . . 3 1R = [⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R
1615opeq1i 3552 . 2 ⟨1R, 0R⟩ = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R
171, 16eqtr2i 2061 1 ⟨[⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 1
 Colors of variables: wff set class Syntax hints:   = wceq 1243  {cab 2026  ⟨cop 3378   class class class wbr 3764  (class class class)co 5512  1𝑜c1o 5994  [cec 6104   ~Q ceq 6377  1Qc1q 6379
 Copyright terms: Public domain W3C validator