Metamath Proof Explorer

Theorem upgrbi

Description: Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 28-Feb-2021)

Ref Expression
Hypotheses upgrbi.x ⊢ X ∈ V
upgrbi.y ⊢ Y ∈ V
Assertion upgrbi ⊢ X Y ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2

Proof

Step Hyp Ref Expression
1 upgrbi.x ⊢ X ∈ V
2 upgrbi.y ⊢ Y ∈ V
3 prssi ⊢ X ∈ V ∧ Y ∈ V → X Y ⊆ V
4 1 2 3 mp2an ⊢ X Y ⊆ V
5 prex ⊢ X Y ∈ V
6 5 elpw ⊢ X Y ∈ 𝒫 V ↔ X Y ⊆ V
7 4 6 mpbir ⊢ X Y ∈ 𝒫 V
8 1 elexi ⊢ X ∈ V
9 8 prnz ⊢ X Y ≠ ∅
10 eldifsn ⊢ X Y ∈ 𝒫 V ∖ ∅ ↔ X Y ∈ 𝒫 V ∧ X Y ≠ ∅
11 7 9 10 mpbir2an ⊢ X Y ∈ 𝒫 V ∖ ∅
12 hashprlei ⊢ X Y ∈ Fin ∧ X Y ≤ 2
13 12 simpri ⊢ X Y ≤ 2
14 fveq2 ⊢ x = X Y → x = X Y
15 14 breq1d ⊢ x = X Y → x ≤ 2 ↔ X Y ≤ 2
16 15 elrab ⊢ X Y ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ↔ X Y ∈ 𝒫 V ∖ ∅ ∧ X Y ≤ 2
17 11 13 16 mpbir2an ⊢ X Y ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2