Step |
Hyp |
Ref |
Expression |
1 |
|
leweon.1 |
⊢ 𝐿 = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } |
2 |
|
epweon |
⊢ E We On |
3 |
|
fvex |
⊢ ( 1st ‘ 𝑦 ) ∈ V |
4 |
3
|
epeli |
⊢ ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ↔ ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ) |
5 |
|
fvex |
⊢ ( 2nd ‘ 𝑦 ) ∈ V |
6 |
5
|
epeli |
⊢ ( ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) |
7 |
6
|
anbi2i |
⊢ ( ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ) ↔ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) |
8 |
4 7
|
orbi12i |
⊢ ( ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ) ) ↔ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) |
9 |
8
|
anbi2i |
⊢ ( ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) ) |
10 |
9
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ) ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } |
11 |
1 10
|
eqtr4i |
⊢ 𝐿 = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ) ) ) } |
12 |
11
|
wexp |
⊢ ( ( E We On ∧ E We On ) → 𝐿 We ( On × On ) ) |
13 |
2 2 12
|
mp2an |
⊢ 𝐿 We ( On × On ) |