Step |
Hyp |
Ref |
Expression |
1 |
|
df-ov |
⊢ ( 𝐼 ∈𝑔 𝐽 ) = ( ∈𝑔 ‘ 〈 𝐼 , 𝐽 〉 ) |
2 |
|
df-goel |
⊢ ∈𝑔 = ( 𝑥 ∈ ( ω × ω ) ↦ 〈 ∅ , 𝑥 〉 ) |
3 |
2
|
a1i |
⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ∈𝑔 = ( 𝑥 ∈ ( ω × ω ) ↦ 〈 ∅ , 𝑥 〉 ) ) |
4 |
|
opeq2 |
⊢ ( 𝑥 = 〈 𝐼 , 𝐽 〉 → 〈 ∅ , 𝑥 〉 = 〈 ∅ , 〈 𝐼 , 𝐽 〉 〉 ) |
5 |
4
|
adantl |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑥 = 〈 𝐼 , 𝐽 〉 ) → 〈 ∅ , 𝑥 〉 = 〈 ∅ , 〈 𝐼 , 𝐽 〉 〉 ) |
6 |
|
opelxpi |
⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → 〈 𝐼 , 𝐽 〉 ∈ ( ω × ω ) ) |
7 |
|
opex |
⊢ 〈 ∅ , 〈 𝐼 , 𝐽 〉 〉 ∈ V |
8 |
7
|
a1i |
⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → 〈 ∅ , 〈 𝐼 , 𝐽 〉 〉 ∈ V ) |
9 |
3 5 6 8
|
fvmptd |
⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( ∈𝑔 ‘ 〈 𝐼 , 𝐽 〉 ) = 〈 ∅ , 〈 𝐼 , 𝐽 〉 〉 ) |
10 |
1 9
|
syl5eq |
⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) = 〈 ∅ , 〈 𝐼 , 𝐽 〉 〉 ) |