Step |
Hyp |
Ref |
Expression |
1 |
|
fneval.1 |
⊢ ∼ = ( Fne ∩ ◡ Fne ) |
2 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) ) |
3 |
|
inss1 |
⊢ ( Fne ∩ ◡ Fne ) ⊆ Fne |
4 |
1 3
|
eqsstri |
⊢ ∼ ⊆ Fne |
5 |
|
fnerel |
⊢ Rel Fne |
6 |
|
relss |
⊢ ( ∼ ⊆ Fne → ( Rel Fne → Rel ∼ ) ) |
7 |
4 5 6
|
mp2 |
⊢ Rel ∼ |
8 |
|
dfrel4v |
⊢ ( Rel ∼ ↔ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∼ 𝑦 } ) |
9 |
7 8
|
mpbi |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∼ 𝑦 } |
10 |
1
|
fneval |
⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 ↔ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) ) ) |
11 |
10
|
el2v |
⊢ ( 𝑥 ∼ 𝑦 ↔ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) ) |
12 |
11
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∼ 𝑦 } = { 〈 𝑥 , 𝑦 〉 ∣ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) } |
13 |
9 12
|
eqtri |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) } |
14 |
2 13
|
eqer |
⊢ ∼ Er V |