Metamath Proof Explorer

Theorem prproropf1olem2

Description: Lemma 2 for prproropf1o . (Contributed by AV, 13-Mar-2023)

Ref Expression
Hypotheses prproropf1o.o ⊢ O = R ∩ V × V
prproropf1o.p ⊢ P = p ∈ 𝒫 V | p = 2
Assertion prproropf1olem2 ⊢ R Or V ∧ X ∈ P → inf X V R sup X V R ∈ O

Proof

Step Hyp Ref Expression
1 prproropf1o.o ⊢ O = R ∩ V × V
2 prproropf1o.p ⊢ P = p ∈ 𝒫 V | p = 2
3 2 prpair ⊢ X ∈ P ↔ ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b
4 simpll ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → R Or V
5 simplrl ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → a ∈ V
6 simplrr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → b ∈ V
7 simprr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → a ≠ b
8 infsupprpr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ a ≠ b → inf a b V R R sup a b V R
9 4 5 6 7 8 syl13anc ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → inf a b V R R sup a b V R
10 df-br ⊢ inf a b V R R sup a b V R ↔ inf a b V R sup a b V R ∈ R
11 9 10 sylib ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → inf a b V R sup a b V R ∈ R
12 infpr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R = if a R b a b
13 ifcl ⊢ a ∈ V ∧ b ∈ V → if a R b a b ∈ V
14 13 3adant1 ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → if a R b a b ∈ V
15 12 14 eqeltrd ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R ∈ V
16 suppr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → sup a b V R = if b R a a b
17 ifcl ⊢ a ∈ V ∧ b ∈ V → if b R a a b ∈ V
18 17 3adant1 ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → if b R a a b ∈ V
19 16 18 eqeltrd ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → sup a b V R ∈ V
20 15 19 jca ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R ∈ V ∧ sup a b V R ∈ V
21 20 3expb ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R ∈ V ∧ sup a b V R ∈ V
22 21 adantr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → inf a b V R ∈ V ∧ sup a b V R ∈ V
23 opelxp ⊢ inf a b V R sup a b V R ∈ V × V ↔ inf a b V R ∈ V ∧ sup a b V R ∈ V
24 22 23 sylibr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → inf a b V R sup a b V R ∈ V × V
25 11 24 elind ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → inf a b V R sup a b V R ∈ R ∩ V × V
26 infeq1 ⊢ X = a b → inf X V R = inf a b V R
27 supeq1 ⊢ X = a b → sup X V R = sup a b V R
28 26 27 opeq12d ⊢ X = a b → inf X V R sup X V R = inf a b V R sup a b V R
29 28 eleq1d ⊢ X = a b → inf X V R sup X V R ∈ R ∩ V × V ↔ inf a b V R sup a b V R ∈ R ∩ V × V
30 29 ad2antrl ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → inf X V R sup X V R ∈ R ∩ V × V ↔ inf a b V R sup a b V R ∈ R ∩ V × V
31 25 30 mpbird ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → inf X V R sup X V R ∈ R ∩ V × V
32 31 ex ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → X = a b ∧ a ≠ b → inf X V R sup X V R ∈ R ∩ V × V
33 32 rexlimdvva ⊢ R Or V → ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b → inf X V R sup X V R ∈ R ∩ V × V
34 3 33 biimtrid ⊢ R Or V → X ∈ P → inf X V R sup X V R ∈ R ∩ V × V
35 34 imp ⊢ R Or V ∧ X ∈ P → inf X V R sup X V R ∈ R ∩ V × V
36 35 1 eleqtrrdi ⊢ R Or V ∧ X ∈ P → inf X V R sup X V R ∈ O