Step |
Hyp |
Ref |
Expression |
1 |
|
niex |
⊢ N ∈ V |
2 |
1 1
|
xpex |
⊢ ( N × N ) ∈ V |
3 |
2 2
|
xpex |
⊢ ( ( N × N ) × ( N × N ) ) ∈ V |
4 |
|
df-enq |
⊢ ~Q = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 〈 𝑧 , 𝑤 〉 ∧ 𝑦 = 〈 𝑣 , 𝑢 〉 ) ∧ ( 𝑧 ·N 𝑢 ) = ( 𝑤 ·N 𝑣 ) ) ) } |
5 |
|
opabssxp |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 〈 𝑧 , 𝑤 〉 ∧ 𝑦 = 〈 𝑣 , 𝑢 〉 ) ∧ ( 𝑧 ·N 𝑢 ) = ( 𝑤 ·N 𝑣 ) ) ) } ⊆ ( ( N × N ) × ( N × N ) ) |
6 |
4 5
|
eqsstri |
⊢ ~Q ⊆ ( ( N × N ) × ( N × N ) ) |
7 |
3 6
|
ssexi |
⊢ ~Q ∈ V |