Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
⊢
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On))
∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
∈ (2nd ‘𝑦))))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1st ‘𝑥)
∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) ∈
(2nd ‘𝑦))))} |
2 | | eleq1w 2817 |
. . . . 5
⊢ (𝑠 = 𝑧 → (𝑠 ∈ (On × On) ↔ 𝑧 ∈ (On ×
On))) |
3 | | eleq1w 2817 |
. . . . 5
⊢ (𝑡 = 𝑤 → (𝑡 ∈ (On × On) ↔ 𝑤 ∈ (On ×
On))) |
4 | 2, 3 | bi2anan9 638 |
. . . 4
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ↔
(𝑧 ∈ (On × On)
∧ 𝑤 ∈ (On ×
On)))) |
5 | | fveq2 6843 |
. . . . . . . 8
⊢ (𝑠 = 𝑧 → (1st ‘𝑠) = (1st ‘𝑧)) |
6 | | fveq2 6843 |
. . . . . . . 8
⊢ (𝑠 = 𝑧 → (2nd ‘𝑠) = (2nd ‘𝑧)) |
7 | 5, 6 | uneq12d 4125 |
. . . . . . 7
⊢ (𝑠 = 𝑧 → ((1st ‘𝑠) ∪ (2nd
‘𝑠)) =
((1st ‘𝑧)
∪ (2nd ‘𝑧))) |
8 | 7 | adantr 482 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1st ‘𝑠) ∪ (2nd
‘𝑠)) =
((1st ‘𝑧)
∪ (2nd ‘𝑧))) |
9 | | fveq2 6843 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (1st ‘𝑡) = (1st ‘𝑤)) |
10 | | fveq2 6843 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (2nd ‘𝑡) = (2nd ‘𝑤)) |
11 | 9, 10 | uneq12d 4125 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((1st ‘𝑡) ∪ (2nd
‘𝑡)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
12 | 11 | adantl 483 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1st ‘𝑡) ∪ (2nd
‘𝑡)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
13 | 8, 12 | eleq12d 2828 |
. . . . 5
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1st ‘𝑠) ∪ (2nd
‘𝑠)) ∈
((1st ‘𝑡)
∪ (2nd ‘𝑡)) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
14 | 7, 11 | eqeqan12d 2747 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1st ‘𝑠) ∪ (2nd
‘𝑠)) =
((1st ‘𝑡)
∪ (2nd ‘𝑡)) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
15 | | breq12 5111 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1st ‘𝑥)
∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) ∈
(2nd ‘𝑦))))}𝑡 ↔ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1st ‘𝑥)
∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) ∈
(2nd ‘𝑦))))}𝑤)) |
16 | 14, 15 | anbi12d 632 |
. . . . 5
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((((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 918 |
. . . 4
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((((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 632 |
. . 3
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((𝑠 ∈ (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 5179 |
. 2
⊢
{⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (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 2733 |
. 2
⊢
({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (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 261 |
. 2
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))) |
22 | | eqid 2733 |
. 2
⊢
((1st ‘𝑤) ∪ (2nd ‘𝑤)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤)) |
23 | | eqid 2733 |
. 2
⊢
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 9954 |
1
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |