Theorem prproropf1olem2

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

	Ref	Expression
Hypotheses	prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
	prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
Assertion	prproropf1olem2	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃 ) → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
2		prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
3	2	prpair	⊢ ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
4		simpll	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → 𝑅 Or 𝑉 )
5		simplrl	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 ∈ 𝑉 )
6		simplrr	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 ∈ 𝑉 )
7		simprr	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 ≠ 𝑏 )
8		infsupprpr	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏 ) ) → inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) 𝑅 sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) )
9	4 5 6 7 8	syl13anc	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) 𝑅 sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) )
10		df-br	⊢ ( inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) 𝑅 sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ↔ ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ ∈ 𝑅 )
11	9 10	sylib	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ ∈ 𝑅 )
12		infpr	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) )
13		ifcl	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ∈ 𝑉 )
14	13	3adant1	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ∈ 𝑉 )
15	12 14	eqeltrd	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 )
16		suppr	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) = if ( 𝑏 𝑅 𝑎 , 𝑎 , 𝑏 ) )
17		ifcl	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → if ( 𝑏 𝑅 𝑎 , 𝑎 , 𝑏 ) ∈ 𝑉 )
18	17	3adant1	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → if ( 𝑏 𝑅 𝑎 , 𝑎 , 𝑏 ) ∈ 𝑉 )
19	16 18	eqeltrd	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 )
20	15 19	jca	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ∧ sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ) )
21	20	3expb	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ∧ sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ) )
22	21	adantr	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ∧ sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ) )
23		opelxp	⊢ ( ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑉 × 𝑉 ) ↔ ( inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ∧ sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ∈ 𝑉 ) )
24	22 23	sylibr	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑉 × 𝑉 ) )
25	11 24	elind	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) )
26		infeq1	⊢ ( 𝑋 = { 𝑎 , 𝑏 } → inf ( 𝑋 , 𝑉 , 𝑅 ) = inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) )
27		supeq1	⊢ ( 𝑋 = { 𝑎 , 𝑏 } → sup ( 𝑋 , 𝑉 , 𝑅 ) = sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) )
28	26 27	opeq12d	⊢ ( 𝑋 = { 𝑎 , 𝑏 } → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ = ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ )
29	28	eleq1d	⊢ ( 𝑋 = { 𝑎 , 𝑏 } → ( ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ↔ ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ) )
30	29	ad2antrl	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ↔ ⟨ inf ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) , sup ( { 𝑎 , 𝑏 } , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ) )
31	25 30	mpbird	⊢ ( ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) )
32	31	ex	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ) )
33	32	rexlimdvva	⊢ ( 𝑅 Or 𝑉 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ) )
34	3 33	syl5bi	⊢ ( 𝑅 Or 𝑉 → ( 𝑋 ∈ 𝑃 → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) ) )
35	34	imp	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃 ) → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ ( 𝑅 ∩ ( 𝑉 × 𝑉 ) ) )
36	35 1	eleqtrrdi	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃 ) → ⟨ inf ( 𝑋 , 𝑉 , 𝑅 ) , sup ( 𝑋 , 𝑉 , 𝑅 ) ⟩ ∈ 𝑂 )