Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } |
2 |
|
eleq1w |
⊢ ( 𝑠 = 𝑧 → ( 𝑠 ∈ ( On × On ) ↔ 𝑧 ∈ ( On × On ) ) ) |
3 |
|
eleq1w |
⊢ ( 𝑡 = 𝑤 → ( 𝑡 ∈ ( On × On ) ↔ 𝑤 ∈ ( On × On ) ) ) |
4 |
2 3
|
bi2anan9 |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ↔ ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ) ) |
5 |
|
fveq2 |
⊢ ( 𝑠 = 𝑧 → ( 1st ‘ 𝑠 ) = ( 1st ‘ 𝑧 ) ) |
6 |
|
fveq2 |
⊢ ( 𝑠 = 𝑧 → ( 2nd ‘ 𝑠 ) = ( 2nd ‘ 𝑧 ) ) |
7 |
5 6
|
uneq12d |
⊢ ( 𝑠 = 𝑧 → ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ) |
9 |
|
fveq2 |
⊢ ( 𝑡 = 𝑤 → ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑤 ) ) |
10 |
|
fveq2 |
⊢ ( 𝑡 = 𝑤 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑤 ) ) |
11 |
9 10
|
uneq12d |
⊢ ( 𝑡 = 𝑤 → ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ) |
13 |
8 12
|
eleq12d |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ↔ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ) ) |
14 |
7 11
|
eqeqan12d |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ↔ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ) ) |
15 |
|
breq12 |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ↔ 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑤 ) ) |
16 |
14 15
|
anbi12d |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ↔ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑤 ) ) ) |
17 |
13 16
|
orbi12d |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∨ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ) ↔ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑤 ) ) ) ) |
18 |
4 17
|
anbi12d |
⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∨ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ) ) ↔ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑤 ) ) ) ) ) |
19 |
18
|
cbvopabv |
⊢ { 〈 𝑠 , 𝑡 〉 ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∨ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ) ) } = { 〈 𝑧 , 𝑤 〉 ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑤 ) ) ) } |
20 |
|
eqid |
⊢ ( { 〈 𝑠 , 𝑡 〉 ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∨ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) = ( { 〈 𝑠 , 𝑡 〉 ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∨ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) |
21 |
|
biid |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) ↔ ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) ) |
22 |
|
eqid |
⊢ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) |
23 |
|
eqid |
⊢ OrdIso ( ( { 〈 𝑠 , 𝑡 〉 ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∨ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) , ( 𝑎 × 𝑎 ) ) = OrdIso ( ( { 〈 𝑠 , 𝑡 〉 ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) ∈ ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∨ ( ( ( 1st ‘ 𝑠 ) ∪ ( 2nd ‘ 𝑠 ) ) = ( ( 1st ‘ 𝑡 ) ∪ ( 2nd ‘ 𝑡 ) ) ∧ 𝑠 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) , ( 𝑎 × 𝑎 ) ) |
24 |
1 19 20 21 22 23
|
infxpenlem |
⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 ) |