prproropf1olem3

	Ref	Expression
Hypotheses	prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
	prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
	prproropf1o.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ )
Assertion	prproropf1olem3	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) → ( 𝐹 ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
2		prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
3		prproropf1o.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ )
4		infeq1	⊢ ( 𝑝 = { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } → inf ( 𝑝 , 𝑉 , 𝑅 ) = inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) )
5		supeq1	⊢ ( 𝑝 = { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } → sup ( 𝑝 , 𝑉 , 𝑅 ) = sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) )
6	4 5	opeq12d	⊢ ( 𝑝 = { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } → ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ = ⟨ inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) , sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) ⟩ )
7	1	prproropf1olem0	⊢ ( 𝑊 ∈ 𝑂 ↔ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
8		simpl	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → 𝑅 Or 𝑉 )
9		simprll	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ( 1^st ‘ 𝑊 ) ∈ 𝑉 )
10		simprlr	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ( 2^nd ‘ 𝑊 ) ∈ 𝑉 )
11		infpr	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) → inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) = if ( ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) , ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ) )
12	8 9 10 11	syl3anc	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) = if ( ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) , ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ) )
13		iftrue	⊢ ( ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) → if ( ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) , ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ) = ( 1^st ‘ 𝑊 ) )
14	13	ad2antll	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → if ( ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) , ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ) = ( 1^st ‘ 𝑊 ) )
15	12 14	eqtrd	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) = ( 1^st ‘ 𝑊 ) )
16		suppr	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) → sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) = if ( ( 2^nd ‘ 𝑊 ) 𝑅 ( 1^st ‘ 𝑊 ) , ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ) )
17	8 9 10 16	syl3anc	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) = if ( ( 2^nd ‘ 𝑊 ) 𝑅 ( 1^st ‘ 𝑊 ) , ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ) )
18		soasym	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ) → ( ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) → ¬ ( 2^nd ‘ 𝑊 ) 𝑅 ( 1^st ‘ 𝑊 ) ) )
19	18	impr	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ¬ ( 2^nd ‘ 𝑊 ) 𝑅 ( 1^st ‘ 𝑊 ) )
20	19	iffalsed	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → if ( ( 2^nd ‘ 𝑊 ) 𝑅 ( 1^st ‘ 𝑊 ) , ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ) = ( 2^nd ‘ 𝑊 ) )
21	17 20	eqtrd	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) = ( 2^nd ‘ 𝑊 ) )
22	15 21	opeq12d	⊢ ( ( 𝑅 Or 𝑉 ∧ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ⟨ inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) , sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) ⟩ = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
23	22	3adantr1	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ⟨ inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) , sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) ⟩ = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
24	7 23	sylan2b	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) → ⟨ inf ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) , sup ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } , 𝑉 , 𝑅 ) ⟩ = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
25	6 24	sylan9eqr	⊢ ( ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) ∧ 𝑝 = { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) → ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
26	1 2	prproropf1olem1	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) → { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝑃 )
27		opex	⊢ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ V
28	27	a1i	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) → ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ V )
29	3 25 26 28	fvmptd2	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) → ( 𝐹 ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )

Metamath Proof Explorer

Theorem prproropf1olem3

Proof