Step | Hyp | Ref
| Expression |
1 | | r0weon.1 |
. . . . 5
⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))} |
2 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (1st ‘𝑥) = (1st ‘𝑧)) |
3 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (2nd ‘𝑥) = (2nd ‘𝑧)) |
4 | 2, 3 | uneq12d 3768 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) =
((1st ‘𝑧)
∪ (2nd ‘𝑧))) |
5 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) = (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
6 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑧) ∈ V |
7 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑧) ∈ V |
8 | 6, 7 | unex 6956 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V |
9 | 4, 5, 8 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) = ((1st ‘𝑧) ∪ (2nd
‘𝑧))) |
10 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (1st ‘𝑥) = (1st ‘𝑤)) |
11 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (2nd ‘𝑥) = (2nd ‘𝑤)) |
12 | 10, 11 | uneq12d 3768 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
13 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑤) ∈ V |
14 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑤) ∈ V |
15 | 13, 14 | unex 6956 |
. . . . . . . . . . 11
⊢
((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V |
16 | 12, 5, 15 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑤) = ((1st ‘𝑤) ∪ (2nd
‘𝑤))) |
17 | 9, 16 | breqan12d 4669 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) E
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
18 | 15 | epelc 5031 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∪ (2nd ‘𝑧)) E ((1st
‘𝑤) ∪
(2nd ‘𝑤))
↔ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st
‘𝑤) ∪
(2nd ‘𝑤))) |
19 | 17, 18 | syl6bb 276 |
. . . . . . . 8
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
20 | 9, 16 | eqeqan12d 2638 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ↔ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
21 | 20 | anbi1d 741 |
. . . . . . . 8
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ ((((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤) ↔ (((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))) |
22 | 19, 21 | orbi12d 746 |
. . . . . . 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 669 |
. . . . . 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 4717 |
. . . . 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 2647 |
. . . 4
⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)))} |
26 | | xp1st 7198 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(1st ‘𝑥)
∈ On) |
27 | | xp2nd 7199 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(2nd ‘𝑥)
∈ On) |
28 | | fvex 6201 |
. . . . . . . . . 10
⊢
(1st ‘𝑥) ∈ V |
29 | 28 | elon 5732 |
. . . . . . . . 9
⊢
((1st ‘𝑥) ∈ On ↔ Ord (1st
‘𝑥)) |
30 | | fvex 6201 |
. . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V |
31 | 30 | elon 5732 |
. . . . . . . . 9
⊢
((2nd ‘𝑥) ∈ On ↔ Ord (2nd
‘𝑥)) |
32 | | ordun 5829 |
. . . . . . . . 9
⊢ ((Ord
(1st ‘𝑥)
∧ Ord (2nd ‘𝑥)) → Ord ((1st ‘𝑥) ∪ (2nd
‘𝑥))) |
33 | 29, 31, 32 | syl2anb 496 |
. . . . . . . 8
⊢
(((1st ‘𝑥) ∈ On ∧ (2nd
‘𝑥) ∈ On) →
Ord ((1st ‘𝑥) ∪ (2nd ‘𝑥))) |
34 | 26, 27, 33 | syl2anc 693 |
. . . . . . 7
⊢ (𝑥 ∈ (On × On) →
Ord ((1st ‘𝑥) ∪ (2nd ‘𝑥))) |
35 | 28, 30 | unex 6956 |
. . . . . . . 8
⊢
((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ V |
36 | 35 | elon 5732 |
. . . . . . 7
⊢
(((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ On ↔ Ord
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
37 | 34, 36 | sylibr 224 |
. . . . . 6
⊢ (𝑥 ∈ (On × On) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ On) |
38 | 5, 37 | fmpti 6383 |
. . . . 5
⊢ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))):(On ×
On)⟶On |
39 | 38 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))):(On ×
On)⟶On) |
40 | | epweon 6983 |
. . . . 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 8834 |
. . . . 5
⊢ 𝐿 We (On ×
On) |
44 | 43 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐿 We (On ×
On)) |
45 | | vex 3203 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
46 | 45 | dmex 7099 |
. . . . . . 7
⊢ dom 𝑢 ∈ V |
47 | 45 | rnex 7100 |
. . . . . . 7
⊢ ran 𝑢 ∈ V |
48 | 46, 47 | unex 6956 |
. . . . . 6
⊢ (dom
𝑢 ∪ ran 𝑢) ∈ V |
49 | | imadmres 5627 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢)) = ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) |
50 | | inss2 3834 |
. . . . . . . . . 10
⊢ (𝑢 ∩ (On × On)) ⊆
(On × On) |
51 | | ssun1 3776 |
. . . . . . . . . . . . . 14
⊢ dom 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
52 | 50 | sseli 3599 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ (On ×
On)) |
53 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (On × On) →
𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉) |
55 | | inss1 3833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ (On × On)) ⊆
𝑢 |
56 | 55 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ 𝑢) |
57 | 54, 56 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑢) |
58 | 28, 30 | opeldm 5328 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑢 → (1st ‘𝑥) ∈ dom 𝑢) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1st ‘𝑥)
∈ dom 𝑢) |
60 | 51, 59 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1st ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
61 | | ssun2 3777 |
. . . . . . . . . . . . . 14
⊢ ran 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
62 | 28, 30 | opelrn 5357 |
. . . . . . . . . . . . . . 15
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑢 → (2nd ‘𝑥) ∈ ran 𝑢) |
63 | 57, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2nd ‘𝑥)
∈ ran 𝑢) |
64 | 61, 63 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2nd ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
65 | | prssi 4353 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) ∈ (dom 𝑢 ∪ ran 𝑢) ∧ (2nd ‘𝑥) ∈ (dom 𝑢 ∪ ran 𝑢)) → {(1st ‘𝑥), (2nd ‘𝑥)} ⊆ (dom 𝑢 ∪ ran 𝑢)) |
66 | 60, 64, 65 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
{(1st ‘𝑥),
(2nd ‘𝑥)}
⊆ (dom 𝑢 ∪ ran
𝑢)) |
67 | 52, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1st ‘𝑥)
∈ On) |
68 | 52, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2nd ‘𝑥)
∈ On) |
69 | | ordunpr 7026 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) ∈ On ∧ (2nd
‘𝑥) ∈ On) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ {(1st ‘𝑥), (2nd ‘𝑥)}) |
70 | 67, 68, 69 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ {(1st ‘𝑥), (2nd ‘𝑥)}) |
71 | 66, 70 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)) |
72 | 71 | rgen 2922 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢) |
73 | | ssrab 3680 |
. . . . . . . . . 10
⊢ ((𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} ↔ ((𝑢 ∩ (On × On)) ⊆ (On ×
On) ∧ ∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢))) |
74 | 50, 72, 73 | mpbir2an 955 |
. . . . . . . . 9
⊢ (𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
75 | | dmres 5419 |
. . . . . . . . . 10
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))) |
76 | 38 | fdmi 6052 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) = (On ×
On) |
77 | 76 | ineq2i 3811 |
. . . . . . . . . 10
⊢ (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))) = (𝑢 ∩ (On × On)) |
78 | 75, 77 | eqtri 2644 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ (On × On)) |
79 | 5 | mptpreima 5628 |
. . . . . . . . 9
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) = {𝑥 ∈ (On × On) ∣
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
80 | 74, 78, 79 | 3sstr4i 3644 |
. . . . . . . 8
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) |
81 | | funmpt 5926 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) |
82 | | resss 5422 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
83 | | dmss 5323 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) → dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥)))) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) |
85 | | funimass3 6333 |
. . . . . . . . 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 𝑢)))) |
86 | 81, 84, 85 | mp2an 708 |
. . . . . . . 8
⊢ (((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) ↔ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢) ⊆ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢))) |
87 | 80, 86 | mpbir 221 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) |
88 | 49, 87 | eqsstr3i 3636 |
. . . . . 6
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ⊆ (dom 𝑢 ∪ ran 𝑢) |
89 | 48, 88 | ssexi 4803 |
. . . . 5
⊢ ((𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ∈ V |
90 | 89 | a1i 11 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ (On
× On) ↦ ((1st ‘𝑥) ∪ (2nd ‘𝑥))) “ 𝑢) ∈ V) |
91 | 25, 39, 41, 44, 90 | fnwe 7293 |
. . 3
⊢ (⊤
→ 𝑅 We (On ×
On)) |
92 | | epse 5097 |
. . . . 5
⊢ E Se
On |
93 | 92 | a1i 11 |
. . . 4
⊢ (⊤
→ E Se On) |
94 | | vuniex 6954 |
. . . . . . . 8
⊢ ∪ 𝑢
∈ V |
95 | 94 | pwex 4848 |
. . . . . . 7
⊢ 𝒫
∪ 𝑢 ∈ V |
96 | 95, 95 | xpex 6962 |
. . . . . 6
⊢
(𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢)
∈ V |
97 | 5 | mptpreima 5628 |
. . . . . . . 8
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) = {𝑥 ∈ (On × On) ∣
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢} |
98 | | df-rab 2921 |
. . . . . . . 8
⊢ {𝑥 ∈ (On × On) ∣
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢} = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢)} |
99 | 97, 98 | eqtri 2644 |
. . . . . . 7
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢)} |
100 | 53 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
101 | | elssuni 4467 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ 𝑢 → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) ⊆ ∪ 𝑢) |
102 | 101 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → ((1st ‘𝑥) ∪ (2nd
‘𝑥)) ⊆ ∪ 𝑢) |
103 | 102 | unssad 3790 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (1st ‘𝑥) ⊆ ∪ 𝑢) |
104 | 28 | elpw 4164 |
. . . . . . . . . . 11
⊢
((1st ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (1st ‘𝑥) ⊆ ∪ 𝑢) |
105 | 103, 104 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (1st ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
106 | 102 | unssbd 3791 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (2nd ‘𝑥) ⊆ ∪ 𝑢) |
107 | 30 | elpw 4164 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (2nd ‘𝑥) ⊆ ∪ 𝑢) |
108 | 106, 107 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → (2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
109 | 105, 108 | jca 554 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → ((1st ‘𝑥) ∈ 𝒫 ∪ 𝑢
∧ (2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢)) |
110 | | elxp6 7200 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) ↔ (𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ ((1st
‘𝑥) ∈ 𝒫
∪ 𝑢 ∧ (2nd ‘𝑥) ∈ 𝒫 ∪ 𝑢))) |
111 | 100, 109,
110 | sylanbrc 698 |
. . . . . . . 8
⊢ ((𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢) → 𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢)) |
112 | 111 | abssi 3677 |
. . . . . . 7
⊢ {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1st ‘𝑥)
∪ (2nd ‘𝑥)) ∈ 𝑢)} ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
113 | 99, 112 | eqsstri 3635 |
. . . . . 6
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
114 | 96, 113 | ssexi 4803 |
. . . . 5
⊢ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ∈ V |
115 | 114 | a1i 11 |
. . . 4
⊢ (⊤
→ (◡(𝑥 ∈ (On × On) ↦
((1st ‘𝑥)
∪ (2nd ‘𝑥))) “ 𝑢) ∈ V) |
116 | 25, 39, 93, 115 | fnse 7294 |
. . 3
⊢ (⊤
→ 𝑅 Se (On ×
On)) |
117 | 91, 116 | jca 554 |
. 2
⊢ (⊤
→ (𝑅 We (On ×
On) ∧ 𝑅 Se (On ×
On))) |
118 | 117 | trud 1493 |
1
⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On ×
On)) |