Step |
Hyp |
Ref |
Expression |
1 |
|
umgrbi.x |
⊢ 𝑋 ∈ 𝑉 |
2 |
|
umgrbi.y |
⊢ 𝑌 ∈ 𝑉 |
3 |
|
umgrbi.n |
⊢ 𝑋 ≠ 𝑌 |
4 |
|
prssi |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 ) |
5 |
1 2 4
|
mp2an |
⊢ { 𝑋 , 𝑌 } ⊆ 𝑉 |
6 |
|
prex |
⊢ { 𝑋 , 𝑌 } ∈ V |
7 |
6
|
elpw |
⊢ ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ↔ { 𝑋 , 𝑌 } ⊆ 𝑉 ) |
8 |
5 7
|
mpbir |
⊢ { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 |
9 |
|
hashprg |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ≠ 𝑌 ↔ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 ) ) |
10 |
3 9
|
mpbii |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 ) |
11 |
1 2 10
|
mp2an |
⊢ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 |
12 |
|
fveqeq2 |
⊢ ( 𝑥 = { 𝑋 , 𝑌 } → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 ) ) |
13 |
12
|
elrab |
⊢ ( { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 ) ) |
14 |
8 11 13
|
mpbir2an |
⊢ { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } |