prproropf1olem1

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

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
2		prproropf1o.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
3	1	prproropf1olem0	⊢ ( 𝑊 ∈ 𝑂 ↔ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) )
4		simpr2	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) )
5		prelpwi	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) → { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝒫 𝑉 )
6	4 5	syl	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝒫 𝑉 )
7		sopo	⊢ ( 𝑅 Or 𝑉 → 𝑅 Po 𝑉 )
8	7	adantr	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → 𝑅 Po 𝑉 )
9		simpr3	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) )
10		po2ne	⊢ ( ( 𝑅 Po 𝑉 ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) → ( 1^st ‘ 𝑊 ) ≠ ( 2^nd ‘ 𝑊 ) )
11	8 4 9 10	syl3anc	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ( 1^st ‘ 𝑊 ) ≠ ( 2^nd ‘ 𝑊 ) )
12		fvex	⊢ ( 1^st ‘ 𝑊 ) ∈ V
13		fvex	⊢ ( 2^nd ‘ 𝑊 ) ∈ V
14		hashprg	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ V ∧ ( 2^nd ‘ 𝑊 ) ∈ V ) → ( ( 1^st ‘ 𝑊 ) ≠ ( 2^nd ‘ 𝑊 ) ↔ ( ♯ ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = 2 ) )
15	12 13 14	mp2an	⊢ ( ( 1^st ‘ 𝑊 ) ≠ ( 2^nd ‘ 𝑊 ) ↔ ( ♯ ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = 2 )
16	11 15	sylib	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ( ♯ ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = 2 )
17	6 16	jca	⊢ ( ( 𝑅 Or 𝑉 ∧ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑊 ) ∈ 𝑉 ) ∧ ( 1^st ‘ 𝑊 ) 𝑅 ( 2^nd ‘ 𝑊 ) ) ) → ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = 2 ) )
18	3 17	sylan2b	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) → ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = 2 ) )
19		fveqeq2	⊢ ( 𝑝 = { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ( ♯ ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = 2 ) )
20	19 2	elrab2	⊢ ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝑃 ↔ ( { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ) = 2 ) )
21	18 20	sylibr	⊢ ( ( 𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂 ) → { ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) } ∈ 𝑃 )

Metamath Proof Explorer

Theorem prproropf1olem1

Proof