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

Theorem ltdfpr 7256
 Description: More convenient form of df-iltp 7220. (Contributed by Jim Kingdon, 15-Dec-2019.)
Assertion
Ref Expression
ltdfpr ((𝐴P𝐵P) → (𝐴<P 𝐵 ↔ ∃𝑞Q (𝑞 ∈ (2nd𝐴) ∧ 𝑞 ∈ (1st𝐵))))
Distinct variable groups:   𝐴,𝑞   𝐵,𝑞

Proof of Theorem ltdfpr
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 3894 . . 3 (𝐴<P 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ <P )
2 df-iltp 7220 . . . 4 <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
32eleq2i 2179 . . 3 (⟨𝐴, 𝐵⟩ ∈ <P ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))})
41, 3bitri 183 . 2 (𝐴<P 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))})
5 simpl 108 . . . . . . 7 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝐴)
65fveq2d 5377 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → (2nd𝑥) = (2nd𝐴))
76eleq2d 2182 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑞 ∈ (2nd𝑥) ↔ 𝑞 ∈ (2nd𝐴)))
8 simpr 109 . . . . . . 7 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑦 = 𝐵)
98fveq2d 5377 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → (1st𝑦) = (1st𝐵))
109eleq2d 2182 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑞 ∈ (1st𝑦) ↔ 𝑞 ∈ (1st𝐵)))
117, 10anbi12d 462 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → ((𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)) ↔ (𝑞 ∈ (2nd𝐴) ∧ 𝑞 ∈ (1st𝐵))))
1211rexbidv 2410 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)) ↔ ∃𝑞Q (𝑞 ∈ (2nd𝐴) ∧ 𝑞 ∈ (1st𝐵))))
1312opelopab2a 4145 . 2 ((𝐴P𝐵P) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))} ↔ ∃𝑞Q (𝑞 ∈ (2nd𝐴) ∧ 𝑞 ∈ (1st𝐵))))
144, 13syl5bb 191 1 ((𝐴P𝐵P) → (𝐴<P 𝐵 ↔ ∃𝑞Q (𝑞 ∈ (2nd𝐴) ∧ 𝑞 ∈ (1st𝐵))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1312   ∈ wcel 1461  ∃wrex 2389  ⟨cop 3494   class class class wbr 3893  {copab 3946  ‘cfv 5079  1st c1st 5988  2nd c2nd 5989  Qcnq 7030  Pcnp 7041
 Copyright terms: Public domain W3C validator