Step | Hyp | Ref
| Expression |
1 | | r0weon.1 |
. . . . 5
⊢ 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) ∈ ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∨
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) = ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∧ 𝑧𝐿𝑤)))} |
2 | | fveq2 6649 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (1^{st} ‘𝑥) = (1^{st} ‘𝑧)) |
3 | | fveq2 6649 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑧)) |
4 | 2, 3 | uneq12d 4094 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) =
((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧))) |
5 | | eqid 2801 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) = (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
6 | | fvex 6662 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑧) ∈ V |
7 | | fvex 6662 |
. . . . . . . . . . . 12
⊢
(2^{nd} ‘𝑧) ∈ V |
8 | 6, 7 | unex 7453 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑧) ∪ (2^{nd} ‘𝑧)) ∈ V |
9 | 4, 5, 8 | fvmpt 6749 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) = ((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧))) |
10 | | fveq2 6649 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (1^{st} ‘𝑥) = (1^{st} ‘𝑤)) |
11 | | fveq2 6649 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑤)) |
12 | 10, 11 | uneq12d 4094 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤))) |
13 | | fvex 6662 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑤) ∈ V |
14 | | fvex 6662 |
. . . . . . . . . . . 12
⊢
(2^{nd} ‘𝑤) ∈ V |
15 | 13, 14 | unex 7453 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑤) ∪ (2^{nd} ‘𝑤)) ∈ V |
16 | 12, 5, 15 | fvmpt 6749 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑤) = ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤))) |
17 | 9, 16 | breqan12d 5049 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ↔ ((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) E
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)))) |
18 | 15 | epeli 5436 |
. . . . . . . . 9
⊢
(((1^{st} ‘𝑧) ∪ (2^{nd} ‘𝑧)) E ((1^{st}
‘𝑤) ∪
(2^{nd} ‘𝑤))
↔ ((1^{st} ‘𝑧) ∪ (2^{nd} ‘𝑧)) ∈ ((1^{st}
‘𝑤) ∪
(2^{nd} ‘𝑤))) |
19 | 17, 18 | syl6bb 290 |
. . . . . . . 8
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ↔ ((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) ∈
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)))) |
20 | 9, 16 | eqeqan12d 2818 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ (((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ↔ ((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)))) |
21 | 20 | anbi1d 632 |
. . . . . . . 8
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ ((((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤) ↔ (((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)) ∧ 𝑧𝐿𝑤))) |
22 | 19, 21 | orbi12d 916 |
. . . . . . 7
⊢ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
→ ((((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)) ↔ (((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) ∈
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)) ∨ (((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
23 | 22 | pm5.32i 578 |
. . . . . 6
⊢ (((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
∧ (((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤))) ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) ∈ ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∨
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) = ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
24 | 23 | opabbii 5100 |
. . . . 5
⊢
{⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧
𝑤 ∈ (On × On))
∧ (((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)))} = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) ∈ ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∨
(((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧)) = ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤)) ∧ 𝑧𝐿𝑤)))} |
25 | 1, 24 | eqtr4i 2827 |
. . . 4
⊢ 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) E ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∨ (((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑧) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))‘𝑤) ∧ 𝑧𝐿𝑤)))} |
26 | | xp1st 7707 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(1^{st} ‘𝑥)
∈ On) |
27 | | xp2nd 7708 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(2^{nd} ‘𝑥)
∈ On) |
28 | | fvex 6662 |
. . . . . . . . . 10
⊢
(1^{st} ‘𝑥) ∈ V |
29 | 28 | elon 6172 |
. . . . . . . . 9
⊢
((1^{st} ‘𝑥) ∈ On ↔ Ord (1^{st}
‘𝑥)) |
30 | | fvex 6662 |
. . . . . . . . . 10
⊢
(2^{nd} ‘𝑥) ∈ V |
31 | 30 | elon 6172 |
. . . . . . . . 9
⊢
((2^{nd} ‘𝑥) ∈ On ↔ Ord (2^{nd}
‘𝑥)) |
32 | | ordun 6264 |
. . . . . . . . 9
⊢ ((Ord
(1^{st} ‘𝑥)
∧ Ord (2^{nd} ‘𝑥)) → Ord ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥))) |
33 | 29, 31, 32 | syl2anb 600 |
. . . . . . . 8
⊢
(((1^{st} ‘𝑥) ∈ On ∧ (2^{nd}
‘𝑥) ∈ On) →
Ord ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) |
34 | 26, 27, 33 | syl2anc 587 |
. . . . . . 7
⊢ (𝑥 ∈ (On × On) →
Ord ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) |
35 | 28, 30 | unex 7453 |
. . . . . . . 8
⊢
((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ V |
36 | 35 | elon 6172 |
. . . . . . 7
⊢
(((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ On ↔ Ord
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
37 | 34, 36 | sylibr 237 |
. . . . . 6
⊢ (𝑥 ∈ (On × On) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ On) |
38 | 5, 37 | fmpti 6857 |
. . . . 5
⊢ (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))):(On ×
On)⟶On |
39 | 38 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))):(On ×
On)⟶On) |
40 | | epweon 7481 |
. . . . 5
⊢ E We
On |
41 | 40 | a1i 11 |
. . . 4
⊢ (⊤
→ E We On) |
42 | | leweon.1 |
. . . . . 6
⊢ 𝐿 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1^{st} ‘𝑥)
∈ (1^{st} ‘𝑦) ∨ ((1^{st} ‘𝑥) = (1^{st} ‘𝑦) ∧ (2^{nd}
‘𝑥) ∈
(2^{nd} ‘𝑦))))} |
43 | 42 | leweon 9426 |
. . . . 5
⊢ 𝐿 We (On ×
On) |
44 | 43 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐿 We (On ×
On)) |
45 | | vex 3447 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
46 | 45 | dmex 7602 |
. . . . . . 7
⊢ dom 𝑢 ∈ V |
47 | 45 | rnex 7603 |
. . . . . . 7
⊢ ran 𝑢 ∈ V |
48 | 46, 47 | unex 7453 |
. . . . . 6
⊢ (dom
𝑢 ∪ ran 𝑢) ∈ V |
49 | | imadmres 6062 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢)) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) |
50 | | inss2 4159 |
. . . . . . . . . 10
⊢ (𝑢 ∩ (On × On)) ⊆
(On × On) |
51 | | ssun1 4102 |
. . . . . . . . . . . . . 14
⊢ dom 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
52 | | elinel2 4126 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ (On ×
On)) |
53 | | 1st2nd2 7714 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (On × On) →
𝑥 = ⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 = ⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩) |
55 | | elinel1 4125 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ 𝑢) |
56 | 54, 55 | eqeltrrd 2894 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∈ 𝑢) |
57 | 28, 30 | opeldm 5744 |
. . . . . . . . . . . . . . 15
⊢
(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∈ 𝑢 → (1^{st} ‘𝑥) ∈ dom 𝑢) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1^{st} ‘𝑥)
∈ dom 𝑢) |
59 | 51, 58 | sseldi 3916 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1^{st} ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
60 | | ssun2 4103 |
. . . . . . . . . . . . . 14
⊢ ran 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
61 | 28, 30 | opelrn 5781 |
. . . . . . . . . . . . . . 15
⊢
(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∈ 𝑢 → (2^{nd} ‘𝑥) ∈ ran 𝑢) |
62 | 56, 61 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2^{nd} ‘𝑥)
∈ ran 𝑢) |
63 | 60, 62 | sseldi 3916 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2^{nd} ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
64 | 59, 63 | prssd 4718 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
{(1^{st} ‘𝑥),
(2^{nd} ‘𝑥)}
⊆ (dom 𝑢 ∪ ran
𝑢)) |
65 | 52, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1^{st} ‘𝑥)
∈ On) |
66 | 52, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2^{nd} ‘𝑥)
∈ On) |
67 | | ordunpr 7525 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑥) ∈ On ∧ (2^{nd}
‘𝑥) ∈ On) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ {(1^{st} ‘𝑥), (2^{nd} ‘𝑥)}) |
68 | 65, 66, 67 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ {(1^{st} ‘𝑥), (2^{nd} ‘𝑥)}) |
69 | 64, 68 | sseldd 3919 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)) |
70 | 69 | rgen 3119 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢) |
71 | | ssrab 4003 |
. . . . . . . . . 10
⊢ ((𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} ↔ ((𝑢 ∩ (On × On)) ⊆ (On ×
On) ∧ ∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢))) |
72 | 50, 70, 71 | mpbir2an 710 |
. . . . . . . . 9
⊢ (𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
73 | | dmres 5844 |
. . . . . . . . . 10
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))) |
74 | 38 | fdmi 6502 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) = (On ×
On) |
75 | 74 | ineq2i 4139 |
. . . . . . . . . 10
⊢ (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))) = (𝑢 ∩ (On × On)) |
76 | 73, 75 | eqtri 2824 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ (On × On)) |
77 | 5 | mptpreima 6063 |
. . . . . . . . 9
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) = {𝑥 ∈ (On × On) ∣
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
78 | 72, 76, 77 | 3sstr4i 3961 |
. . . . . . . 8
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) |
79 | | funmpt 6366 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) |
80 | | resss 5847 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
81 | | dmss 5739 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) → dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))) |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
83 | | funimass3 6805 |
. . . . . . . . 9
⊢ ((Fun
(𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ∧ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))) → (((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) ↔ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)))) |
84 | 79, 82, 83 | mp2an 691 |
. . . . . . . 8
⊢ (((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) ↔ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢))) |
85 | 78, 84 | mpbir 234 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) |
86 | 49, 85 | eqsstrri 3953 |
. . . . . 6
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ⊆ (dom 𝑢 ∪ ran 𝑢) |
87 | 48, 86 | ssexi 5193 |
. . . . 5
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V |
88 | 87 | a1i 11 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V) |
89 | 25, 39, 41, 44, 88 | fnwe 7813 |
. . 3
⊢ (⊤
→ 𝑅 We (On ×
On)) |
90 | | epse 5506 |
. . . . 5
⊢ E Se
On |
91 | 90 | a1i 11 |
. . . 4
⊢ (⊤
→ E Se On) |
92 | | vuniex 7449 |
. . . . . . . 8
⊢ ∪ 𝑢
∈ V |
93 | 92 | pwex 5249 |
. . . . . . 7
⊢ 𝒫
∪ 𝑢 ∈ V |
94 | 93, 93 | xpex 7460 |
. . . . . 6
⊢
(𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢)
∈ V |
95 | 5 | mptpreima 6063 |
. . . . . . . 8
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) = {𝑥 ∈ (On × On) ∣
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢} |
96 | | df-rab 3118 |
. . . . . . . 8
⊢ {𝑥 ∈ (On × On) ∣
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢} = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢)} |
97 | 95, 96 | eqtri 2824 |
. . . . . . 7
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢)} |
98 | 53 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
99 | | elssuni 4833 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ 𝑢 → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) ⊆ ∪ 𝑢) |
100 | 99 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) ⊆ ∪ 𝑢) |
101 | 100 | unssad 4117 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (1^{st} ‘𝑥) ⊆ ∪ 𝑢) |
102 | 28 | elpw 4504 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (1^{st} ‘𝑥) ⊆ ∪ 𝑢) |
103 | 101, 102 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (1^{st} ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
104 | 100 | unssbd 4118 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (2^{nd} ‘𝑥) ⊆ ∪ 𝑢) |
105 | 30 | elpw 4504 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (2^{nd} ‘𝑥) ⊆ ∪ 𝑢) |
106 | 104, 105 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
107 | 103, 106 | jca 515 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → ((1^{st} ‘𝑥) ∈ 𝒫 ∪ 𝑢
∧ (2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢)) |
108 | | elxp6 7709 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) ↔ (𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∧ ((1^{st}
‘𝑥) ∈ 𝒫
∪ 𝑢 ∧ (2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢))) |
109 | 98, 107, 108 | sylanbrc 586 |
. . . . . . . 8
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → 𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢)) |
110 | 109 | abssi 4000 |
. . . . . . 7
⊢ {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢)} ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
111 | 97, 110 | eqsstri 3952 |
. . . . . 6
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
112 | 94, 111 | ssexi 5193 |
. . . . 5
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V |
113 | 112 | a1i 11 |
. . . 4
⊢ (⊤
→ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V) |
114 | 25, 39, 91, 113 | fnse 7814 |
. . 3
⊢ (⊤
→ 𝑅 Se (On ×
On)) |
115 | 89, 114 | jca 515 |
. 2
⊢ (⊤
→ (𝑅 We (On ×
On) ∧ 𝑅 Se (On ×
On))) |
116 | 115 | mptru 1545 |
1
⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On ×
On)) |