Step | Hyp | Ref
| Expression |
1 | | eqid 2778 |
. 2
⊢
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On))
∧ ((1^{st} ‘𝑥) ∈ (1^{st} ‘𝑦) ∨ ((1^{st}
‘𝑥) = (1^{st}
‘𝑦) ∧
(2^{nd} ‘𝑥)
∈ (2^{nd} ‘𝑦))))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))} |
2 | | eleq1w 2842 |
. . . . 5
⊢ (𝑠 = 𝑧 → (𝑠 ∈ (On × On) ↔ 𝑧 ∈ (On ×
On))) |
3 | | eleq1w 2842 |
. . . . 5
⊢ (𝑡 = 𝑤 → (𝑡 ∈ (On × On) ↔ 𝑤 ∈ (On ×
On))) |
4 | 2, 3 | bi2anan9 629 |
. . . 4
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ↔
(𝑧 ∈ (On × On)
∧ 𝑤 ∈ (On ×
On)))) |
5 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑠 = 𝑧 → (1^{st} ‘𝑠) = (1^{st} ‘𝑧)) |
6 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑠 = 𝑧 → (2^{nd} ‘𝑠) = (2^{nd} ‘𝑧)) |
7 | 5, 6 | uneq12d 3991 |
. . . . . . 7
⊢ (𝑠 = 𝑧 → ((1^{st} ‘𝑠) ∪ (2^{nd}
‘𝑠)) =
((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧))) |
8 | 7 | adantr 474 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^{st} ‘𝑠) ∪ (2^{nd}
‘𝑠)) =
((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧))) |
9 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (1^{st} ‘𝑡) = (1^{st} ‘𝑤)) |
10 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑤)) |
11 | 9, 10 | uneq12d 3991 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤))) |
12 | 11 | adantl 475 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤))) |
13 | 8, 12 | eleq12d 2853 |
. . . . 5
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^{st} ‘𝑠) ∪ (2^{nd}
‘𝑠)) ∈
((1^{st} ‘𝑡)
∪ (2^{nd} ‘𝑡)) ↔ ((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) ∈
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)))) |
14 | 7, 11 | eqeqan12d 2794 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^{st} ‘𝑠) ∪ (2^{nd}
‘𝑠)) =
((1^{st} ‘𝑡)
∪ (2^{nd} ‘𝑡)) ↔ ((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)))) |
15 | | breq12 4891 |
. . . . . 6
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡 ↔ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑤)) |
16 | 14, 15 | anbi12d 624 |
. . . . 5
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((((1^{st} ‘𝑠) ∪ (2^{nd}
‘𝑠)) =
((1^{st} ‘𝑡)
∪ (2^{nd} ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡) ↔ (((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑤))) |
17 | 13, 16 | orbi12d 905 |
. . . 4
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((((1^{st} ‘𝑠) ∪ (2^{nd}
‘𝑠)) ∈
((1^{st} ‘𝑡)
∪ (2^{nd} ‘𝑡)) ∨ (((1^{st} ‘𝑠) ∪ (2^{nd}
‘𝑠)) =
((1^{st} ‘𝑡)
∪ (2^{nd} ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡)) ↔ (((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) ∈
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)) ∨ (((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑤)))) |
18 | 4, 17 | anbi12d 624 |
. . 3
⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧
(((1^{st} ‘𝑠)
∪ (2^{nd} ‘𝑠)) ∈ ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) ∨
(((1^{st} ‘𝑠)
∪ (2^{nd} ‘𝑠)) = ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡))) ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) ∈ ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∨
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) = ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑤))))) |
19 | 18 | cbvopabv 4958 |
. 2
⊢
{⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧
𝑡 ∈ (On × On))
∧ (((1^{st} ‘𝑠) ∪ (2^{nd} ‘𝑠)) ∈ ((1^{st}
‘𝑡) ∪
(2^{nd} ‘𝑡))
∨ (((1^{st} ‘𝑠) ∪ (2^{nd} ‘𝑠)) = ((1^{st}
‘𝑡) ∪
(2^{nd} ‘𝑡))
∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡)))} = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) ∈ ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∨
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) = ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑤)))} |
20 | | eqid 2778 |
. 2
⊢
({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧
𝑡 ∈ (On × On))
∧ (((1^{st} ‘𝑠) ∪ (2^{nd} ‘𝑠)) ∈ ((1^{st}
‘𝑡) ∪
(2^{nd} ‘𝑡))
∨ (((1^{st} ‘𝑠) ∪ (2^{nd} ‘𝑠)) = ((1^{st}
‘𝑡) ∪
(2^{nd} ‘𝑡))
∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) = ({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧
(((1^{st} ‘𝑠)
∪ (2^{nd} ‘𝑠)) ∈ ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) ∨
(((1^{st} ‘𝑠)
∪ (2^{nd} ‘𝑠)) = ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) |
21 | | biid 253 |
. 2
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))) |
22 | | eqid 2778 |
. 2
⊢
((1^{st} ‘𝑤) ∪ (2^{nd} ‘𝑤)) = ((1^{st}
‘𝑤) ∪
(2^{nd} ‘𝑤)) |
23 | | eqid 2778 |
. 2
⊢
OrdIso(({⟨𝑠,
𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧
𝑡 ∈ (On × On))
∧ (((1^{st} ‘𝑠) ∪ (2^{nd} ‘𝑠)) ∈ ((1^{st}
‘𝑡) ∪
(2^{nd} ‘𝑡))
∨ (((1^{st} ‘𝑠) ∪ (2^{nd} ‘𝑠)) = ((1^{st}
‘𝑡) ∪
(2^{nd} ‘𝑡))
∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))), (𝑎 × 𝑎)) = OrdIso(({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧
(((1^{st} ‘𝑠)
∪ (2^{nd} ‘𝑠)) ∈ ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) ∨
(((1^{st} ‘𝑠)
∪ (2^{nd} ‘𝑠)) = ((1^{st} ‘𝑡) ∪ (2^{nd}
‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))), (𝑎 × 𝑎)) |
24 | 1, 19, 20, 21, 22, 23 | infxpenlem 9169 |
1
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |