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

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

Proof of Theorem pitonnlem1
StepHypRef Expression
1 df-1 7672 . 2 1 = ⟨1R, 0R
2 df-1r 7584 . . . 4 1R = [⟨(1P +P 1P), 1P⟩] ~R
3 df-i1p 7319 . . . . . . . 8 1P = ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
4 df-1nqqs 7203 . . . . . . . . . . 11 1Q = [⟨1o, 1o⟩] ~Q
54breq2i 3946 . . . . . . . . . 10 (𝑙 <Q 1Q𝑙 <Q [⟨1o, 1o⟩] ~Q )
65abbii 2256 . . . . . . . . 9 {𝑙𝑙 <Q 1Q} = {𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }
74breq1i 3945 . . . . . . . . . 10 (1Q <Q 𝑢 ↔ [⟨1o, 1o⟩] ~Q <Q 𝑢)
87abbii 2256 . . . . . . . . 9 {𝑢 ∣ 1Q <Q 𝑢} = {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}
96, 8opeq12i 3719 . . . . . . . 8 ⟨{𝑙𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩
103, 9eqtri 2161 . . . . . . 7 1P = ⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩
1110oveq1i 5793 . . . . . 6 (1P +P 1P) = (⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P)
1211opeq1i 3717 . . . . 5 ⟨(1P +P 1P), 1P⟩ = ⟨(⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P
13 eceq1 6473 . . . . 5 (⟨(1P +P 1P), 1P⟩ = ⟨(⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ → [⟨(1P +P 1P), 1P⟩] ~R = [⟨(⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
1412, 13ax-mp 5 . . . 4 [⟨(1P +P 1P), 1P⟩] ~R = [⟨(⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R
152, 14eqtri 2161 . . 3 1R = [⟨(⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R
1615opeq1i 3717 . 2 ⟨1R, 0R⟩ = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R
171, 16eqtr2i 2162 1 ⟨[⟨(⟨{𝑙𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 1
 Colors of variables: wff set class Syntax hints:   = wceq 1332  {cab 2126  ⟨cop 3536   class class class wbr 3938  (class class class)co 5783  1oc1o 6315  [cec 6436   ~Q ceq 7131  1Qc1q 7133
 Copyright terms: Public domain W3C validator