| Step | Hyp | Ref
| Expression |
| 1 | | r0weon.1 |
. . . . 5
⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))} |
| 2 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (1st ‘𝑥) = (1st ‘𝑧)) |
| 3 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (2nd ‘𝑥) = (2nd ‘𝑧)) |
| 4 | 2, 3 | uneq12d 4169 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) =
((1st ‘𝑧)
∪ (2nd ‘𝑧))) |
| 5 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) = (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
| 6 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑧) ∈ V |
| 7 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑧) ∈ V |
| 8 | 6, 7 | unex 7764 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V |
| 9 | 4, 5, 8 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) = ((1st ‘𝑧) ∪ (2nd
‘𝑧))) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (1st ‘𝑥) = (1st ‘𝑤)) |
| 11 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (2nd ‘𝑥) = (2nd ‘𝑤)) |
| 12 | 10, 11 | uneq12d 4169 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
| 13 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑤) ∈ V |
| 14 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑤) ∈ V |
| 15 | 13, 14 | unex 7764 |
. . . . . . . . . . 11
⊢
((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V |
| 16 | 12, 5, 15 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑤) = ((1st ‘𝑤) ∪ (2nd
‘𝑤))) |
| 17 | 9, 16 | breqan12d 5159 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) E
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
| 18 | 15 | epeli 5586 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∪ (2nd ‘𝑧)) E ((1st
‘𝑤) ∪
(2nd ‘𝑤))
↔ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st
‘𝑤) ∪
(2nd ‘𝑤))) |
| 19 | 17, 18 | bitrdi 287 |
. . . . . . . 8
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
| 20 | 9, 16 | eqeqan12d 2751 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
| 21 | 20 | anbi1d 631 |
. . . . . . . 8
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ ((((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤) ↔ (((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))) |
| 22 | 19, 21 | orbi12d 919 |
. . . . . . 7
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ ((((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)) ↔ (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
| 23 | 22 | pm5.32i 574 |
. . . . . 6
⊢ (((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
∧ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤))) ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
| 24 | 23 | opabbii 5210 |
. . . . 5
⊢
{〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
∧ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)))} = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))} |
| 25 | 1, 24 | eqtr4i 2768 |
. . . 4
⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)))} |
| 26 | | xp1st 8046 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(1st ‘𝑥)
∈ On) |
| 27 | | xp2nd 8047 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(2nd ‘𝑥)
∈ On) |
| 28 | | fvex 6919 |
. . . . . . . . . 10
⊢
(1st ‘𝑥) ∈ V |
| 29 | 28 | elon 6393 |
. . . . . . . . 9
⊢
((1st ‘𝑥) ∈ On ↔ Ord (1st
‘𝑥)) |
| 30 | | fvex 6919 |
. . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V |
| 31 | 30 | elon 6393 |
. . . . . . . . 9
⊢
((2nd ‘𝑥) ∈ On ↔ Ord (2nd
‘𝑥)) |
| 32 | | ordun 6488 |
. . . . . . . . 9
⊢ ((Ord
(1st ‘𝑥)
∧ Ord (2nd ‘𝑥)) → Ord ((1st ‘𝑥) ∪ (2nd
‘𝑥))) |
| 33 | 29, 31, 32 | syl2anb 598 |
. . . . . . . 8
⊢
(((1st ‘𝑥) ∈ On ∧ (2nd
‘𝑥) ∈ On) →
Ord ((1st ‘𝑥) ∪ (2nd ‘𝑥))) |
| 34 | 26, 27, 33 | syl2anc 584 |
. . . . . . 7
⊢ (𝑥 ∈ (On × On) →
Ord ((1st ‘𝑥) ∪ (2nd ‘𝑥))) |
| 35 | 28, 30 | unex 7764 |
. . . . . . . 8
⊢
((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ V |
| 36 | 35 | elon 6393 |
. . . . . . 7
⊢
(((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ On ↔ Ord
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
| 37 | 34, 36 | sylibr 234 |
. . . . . 6
⊢ (𝑥 ∈ (On × On) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ On) |
| 38 | 5, 37 | fmpti 7132 |
. . . . 5
⊢ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))):(On ×
On)⟶On |
| 39 | 38 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))):(On ×
On)⟶On) |
| 40 | | epweon 7795 |
. . . . 5
⊢ E We
On |
| 41 | 40 | a1i 11 |
. . . 4
⊢ (⊤
→ E We On) |
| 42 | | leweon.1 |
. . . . . 6
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1st ‘𝑥)
∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) ∈
(2nd ‘𝑦))))} |
| 43 | 42 | leweon 10051 |
. . . . 5
⊢ 𝐿 We (On ×
On) |
| 44 | 43 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐿 We (On ×
On)) |
| 45 | | vex 3484 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
| 46 | 45 | dmex 7931 |
. . . . . . 7
⊢ dom 𝑢 ∈ V |
| 47 | 45 | rnex 7932 |
. . . . . . 7
⊢ ran 𝑢 ∈ V |
| 48 | 46, 47 | unex 7764 |
. . . . . 6
⊢ (dom
𝑢 ∪ ran 𝑢) ∈ V |
| 49 | | imadmres 6254 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢)) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) |
| 50 | | inss2 4238 |
. . . . . . . . . 10
⊢ (𝑢 ∩ (On × On)) ⊆
(On × On) |
| 51 | | ssun1 4178 |
. . . . . . . . . . . . . 14
⊢ dom 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
| 52 | | elinel2 4202 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ (On ×
On)) |
| 53 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (On × On) →
𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉) |
| 54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉) |
| 55 | | elinel1 4201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ 𝑢) |
| 56 | 54, 55 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑢) |
| 57 | 28, 30 | opeldm 5918 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑢 → (1st ‘𝑥) ∈ dom 𝑢) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1st ‘𝑥)
∈ dom 𝑢) |
| 59 | 51, 58 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1st ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
| 60 | | ssun2 4179 |
. . . . . . . . . . . . . 14
⊢ ran 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
| 61 | 28, 30 | opelrn 5954 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑢 → (2nd ‘𝑥) ∈ ran 𝑢) |
| 62 | 56, 61 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2nd ‘𝑥)
∈ ran 𝑢) |
| 63 | 60, 62 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2nd ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
| 64 | 59, 63 | prssd 4822 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
{(1st ‘𝑥),
(2nd ‘𝑥)}
⊆ (dom 𝑢 ∪ ran
𝑢)) |
| 65 | 52, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1st ‘𝑥)
∈ On) |
| 66 | 52, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2nd ‘𝑥)
∈ On) |
| 67 | | ordunpr 7846 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) ∈ On ∧ (2nd
‘𝑥) ∈ On) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ {(1st ‘𝑥), (2nd ‘𝑥)}) |
| 68 | 65, 66, 67 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ {(1st ‘𝑥), (2nd ‘𝑥)}) |
| 69 | 64, 68 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)) |
| 70 | 69 | rgen 3063 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢) |
| 71 | | ssrab 4073 |
. . . . . . . . . 10
⊢ ((𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} ↔ ((𝑢 ∩ (On × On)) ⊆ (On ×
On) ∧ ∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢))) |
| 72 | 50, 70, 71 | mpbir2an 711 |
. . . . . . . . 9
⊢ (𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
| 73 | | dmres 6030 |
. . . . . . . . . 10
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))) |
| 74 | 38 | fdmi 6747 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) = (On ×
On) |
| 75 | 74 | ineq2i 4217 |
. . . . . . . . . 10
⊢ (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))) = (𝑢 ∩ (On × On)) |
| 76 | 73, 75 | eqtri 2765 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ (On × On)) |
| 77 | 5 | mptpreima 6258 |
. . . . . . . . 9
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) = {𝑥 ∈ (On × On) ∣
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
| 78 | 72, 76, 77 | 3sstr4i 4035 |
. . . . . . . 8
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) |
| 79 | | funmpt 6604 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) |
| 80 | | resss 6019 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
| 81 | | dmss 5913 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) → dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))) |
| 82 | 80, 81 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
| 83 | | funimass3 7074 |
. . . . . . . . 9
⊢ ((Fun
(𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ∧ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))) → (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) ↔ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)))) |
| 84 | 79, 82, 83 | mp2an 692 |
. . . . . . . 8
⊢ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) ↔ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢))) |
| 85 | 78, 84 | mpbir 231 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) |
| 86 | 49, 85 | eqsstrri 4031 |
. . . . . 6
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ⊆ (dom 𝑢 ∪ ran 𝑢) |
| 87 | 48, 86 | ssexi 5322 |
. . . . 5
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ∈ V |
| 88 | 87 | a1i 11 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) “ 𝑢) ∈ V) |
| 89 | 25, 39, 41, 44, 88 | fnwe 8157 |
. . 3
⊢ (⊤
→ 𝑅 We (On ×
On)) |
| 90 | | epse 5667 |
. . . . 5
⊢ E Se
On |
| 91 | 90 | a1i 11 |
. . . 4
⊢ (⊤
→ E Se On) |
| 92 | | vuniex 7759 |
. . . . . . . 8
⊢ ∪ 𝑢
∈ V |
| 93 | 92 | pwex 5380 |
. . . . . . 7
⊢ 𝒫
∪ 𝑢 ∈ V |
| 94 | 93, 93 | xpex 7773 |
. . . . . 6
⊢
(𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢)
∈ V |
| 95 | 5 | mptpreima 6258 |
. . . . . . . 8
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) = {𝑥 ∈ (On × On) ∣
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢} |
| 96 | | df-rab 3437 |
. . . . . . . 8
⊢ {𝑥 ∈ (On × On) ∣
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢} = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢)} |
| 97 | 95, 96 | eqtri 2765 |
. . . . . . 7
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢)} |
| 98 | 53 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
| 99 | | elssuni 4937 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ 𝑢 → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) ⊆ ∪ 𝑢) |
| 100 | 99 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) ⊆ ∪ 𝑢) |
| 101 | 100 | unssad 4193 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (1st ‘𝑥) ⊆ ∪ 𝑢) |
| 102 | 28 | elpw 4604 |
. . . . . . . . . . 11
⊢
((1st ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (1st ‘𝑥) ⊆ ∪ 𝑢) |
| 103 | 101, 102 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (1st ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
| 104 | 100 | unssbd 4194 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (2nd ‘𝑥) ⊆ ∪ 𝑢) |
| 105 | 30 | elpw 4604 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (2nd ‘𝑥) ⊆ ∪ 𝑢) |
| 106 | 104, 105 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
| 107 | 103, 106 | jca 511 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → ((1st ‘𝑥) ∈ 𝒫 ∪ 𝑢
∧ (2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢)) |
| 108 | | elxp6 8048 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) ↔ (𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ ((1st
‘𝑥) ∈ 𝒫
∪ 𝑢 ∧ (2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢))) |
| 109 | 98, 107, 108 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → 𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢)) |
| 110 | 109 | abssi 4070 |
. . . . . . 7
⊢ {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢)} ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
| 111 | 97, 110 | eqsstri 4030 |
. . . . . 6
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
| 112 | 94, 111 | ssexi 5322 |
. . . . 5
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ∈ V |
| 113 | 112 | a1i 11 |
. . . 4
⊢ (⊤
→ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ∈ V) |
| 114 | 25, 39, 91, 113 | fnse 8158 |
. . 3
⊢ (⊤
→ 𝑅 Se (On ×
On)) |
| 115 | 89, 114 | jca 511 |
. 2
⊢ (⊤
→ (𝑅 We (On ×
On) ∧ 𝑅 Se (On ×
On))) |
| 116 | 115 | mptru 1547 |
1
⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On ×
On)) |