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 6229 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (1^{st} ‘𝑥) = (1^{st} ‘𝑧)) |
3 | | fveq2 6229 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑧)) |
4 | 2, 3 | uneq12d 3801 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) =
((1^{st} ‘𝑧)
∪ (2^{nd} ‘𝑧))) |
5 | | eqid 2651 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) = (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
6 | | fvex 6239 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑧) ∈ V |
7 | | fvex 6239 |
. . . . . . . . . . . 12
⊢
(2^{nd} ‘𝑧) ∈ V |
8 | 6, 7 | unex 6998 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑧) ∪ (2^{nd} ‘𝑧)) ∈ V |
9 | 4, 5, 8 | fvmpt 6321 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑧) = ((1^{st} ‘𝑧) ∪ (2^{nd}
‘𝑧))) |
10 | | fveq2 6229 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (1^{st} ‘𝑥) = (1^{st} ‘𝑤)) |
11 | | fveq2 6229 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑤)) |
12 | 10, 11 | uneq12d 3801 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) =
((1^{st} ‘𝑤)
∪ (2^{nd} ‘𝑤))) |
13 | | fvex 6239 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑤) ∈ V |
14 | | fvex 6239 |
. . . . . . . . . . . 12
⊢
(2^{nd} ‘𝑤) ∈ V |
15 | 13, 14 | unex 6998 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑤) ∪ (2^{nd} ‘𝑤)) ∈ V |
16 | 12, 5, 15 | fvmpt 6321 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (On × On) →
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)))‘𝑤) = ((1^{st} ‘𝑤) ∪ (2^{nd}
‘𝑤))) |
17 | 9, 16 | breqan12d 4701 |
. . . . . . . . 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 | epelc 5060 |
. . . . . . . . 9
⊢
(((1^{st} ‘𝑧) ∪ (2^{nd} ‘𝑧)) E ((1^{st}
‘𝑤) ∪
(2^{nd} ‘𝑤))
↔ ((1^{st} ‘𝑧) ∪ (2^{nd} ‘𝑧)) ∈ ((1^{st}
‘𝑤) ∪
(2^{nd} ‘𝑤))) |
19 | 17, 18 | syl6bb 276 |
. . . . . . . 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 2667 |
. . . . . . . . 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 741 |
. . . . . . . 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 746 |
. . . . . . 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 670 |
. . . . . 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 4750 |
. . . . 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 2676 |
. . . 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 7242 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(1^{st} ‘𝑥)
∈ On) |
27 | | xp2nd 7243 |
. . . . . . . 8
⊢ (𝑥 ∈ (On × On) →
(2^{nd} ‘𝑥)
∈ On) |
28 | | fvex 6239 |
. . . . . . . . . 10
⊢
(1^{st} ‘𝑥) ∈ V |
29 | 28 | elon 5770 |
. . . . . . . . 9
⊢
((1^{st} ‘𝑥) ∈ On ↔ Ord (1^{st}
‘𝑥)) |
30 | | fvex 6239 |
. . . . . . . . . 10
⊢
(2^{nd} ‘𝑥) ∈ V |
31 | 30 | elon 5770 |
. . . . . . . . 9
⊢
((2^{nd} ‘𝑥) ∈ On ↔ Ord (2^{nd}
‘𝑥)) |
32 | | ordun 5867 |
. . . . . . . . 9
⊢ ((Ord
(1^{st} ‘𝑥)
∧ Ord (2^{nd} ‘𝑥)) → Ord ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥))) |
33 | 29, 31, 32 | syl2anb 495 |
. . . . . . . 8
⊢
(((1^{st} ‘𝑥) ∈ On ∧ (2^{nd}
‘𝑥) ∈ On) →
Ord ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) |
34 | 26, 27, 33 | syl2anc 694 |
. . . . . . 7
⊢ (𝑥 ∈ (On × On) →
Ord ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) |
35 | 28, 30 | unex 6998 |
. . . . . . . 8
⊢
((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ V |
36 | 35 | elon 5770 |
. . . . . . 7
⊢
(((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ On ↔ Ord
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
37 | 34, 36 | sylibr 224 |
. . . . . 6
⊢ (𝑥 ∈ (On × On) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ On) |
38 | 5, 37 | fmpti 6423 |
. . . . 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 7025 |
. . . . 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 8872 |
. . . . 5
⊢ 𝐿 We (On ×
On) |
44 | 43 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐿 We (On ×
On)) |
45 | | vex 3234 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
46 | 45 | dmex 7141 |
. . . . . . 7
⊢ dom 𝑢 ∈ V |
47 | 45 | rnex 7142 |
. . . . . . 7
⊢ ran 𝑢 ∈ V |
48 | 46, 47 | unex 6998 |
. . . . . 6
⊢ (dom
𝑢 ∪ ran 𝑢) ∈ V |
49 | | imadmres 5665 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢)) = ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) |
50 | | inss2 3867 |
. . . . . . . . . 10
⊢ (𝑢 ∩ (On × On)) ⊆
(On × On) |
51 | | ssun1 3809 |
. . . . . . . . . . . . . 14
⊢ dom 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
52 | 50 | sseli 3632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ (On ×
On)) |
53 | | 1st2nd2 7249 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (On × On) →
𝑥 = ⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 = ⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩) |
55 | | inss1 3866 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ (On × On)) ⊆
𝑢 |
56 | 55 | sseli 3632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) → 𝑥 ∈ 𝑢) |
57 | 54, 56 | eqeltrrd 2731 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∈ 𝑢) |
58 | 28, 30 | opeldm 5360 |
. . . . . . . . . . . . . . 15
⊢
(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∈ 𝑢 → (1^{st} ‘𝑥) ∈ dom 𝑢) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1^{st} ‘𝑥)
∈ dom 𝑢) |
60 | 51, 59 | sseldi 3634 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1^{st} ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
61 | | ssun2 3810 |
. . . . . . . . . . . . . 14
⊢ ran 𝑢 ⊆ (dom 𝑢 ∪ ran 𝑢) |
62 | 28, 30 | opelrn 5389 |
. . . . . . . . . . . . . . 15
⊢
(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∈ 𝑢 → (2^{nd} ‘𝑥) ∈ ran 𝑢) |
63 | 57, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2^{nd} ‘𝑥)
∈ ran 𝑢) |
64 | 61, 63 | sseldi 3634 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2^{nd} ‘𝑥)
∈ (dom 𝑢 ∪ ran
𝑢)) |
65 | | prssi 4385 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑥) ∈ (dom 𝑢 ∪ ran 𝑢) ∧ (2^{nd} ‘𝑥) ∈ (dom 𝑢 ∪ ran 𝑢)) → {(1^{st} ‘𝑥), (2^{nd} ‘𝑥)} ⊆ (dom 𝑢 ∪ ran 𝑢)) |
66 | 60, 64, 65 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
{(1^{st} ‘𝑥),
(2^{nd} ‘𝑥)}
⊆ (dom 𝑢 ∪ ran
𝑢)) |
67 | 52, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(1^{st} ‘𝑥)
∈ On) |
68 | 52, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
(2^{nd} ‘𝑥)
∈ On) |
69 | | ordunpr 7068 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑥) ∈ On ∧ (2^{nd}
‘𝑥) ∈ On) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ {(1^{st} ‘𝑥), (2^{nd} ‘𝑥)}) |
70 | 67, 68, 69 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ {(1^{st} ‘𝑥), (2^{nd} ‘𝑥)}) |
71 | 66, 70 | sseldd 3637 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑢 ∩ (On × On)) →
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)) |
72 | 71 | rgen 2951 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢) |
73 | | ssrab 3713 |
. . . . . . . . . 10
⊢ ((𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} ↔ ((𝑢 ∩ (On × On)) ⊆ (On ×
On) ∧ ∀𝑥 ∈
(𝑢 ∩ (On ×
On))((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢))) |
74 | 50, 72, 73 | mpbir2an 975 |
. . . . . . . . 9
⊢ (𝑢 ∩ (On × On)) ⊆
{𝑥 ∈ (On × On)
∣ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
75 | | dmres 5454 |
. . . . . . . . . 10
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))) |
76 | 38 | fdmi 6090 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) = (On ×
On) |
77 | 76 | ineq2i 3844 |
. . . . . . . . . 10
⊢ (𝑢 ∩ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)))) = (𝑢 ∩ (On × On)) |
78 | 75, 77 | eqtri 2673 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) = (𝑢 ∩ (On × On)) |
79 | 5 | mptpreima 5666 |
. . . . . . . . 9
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) = {𝑥 ∈ (On × On) ∣
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ (dom 𝑢 ∪ ran 𝑢)} |
80 | 74, 78, 79 | 3sstr4i 3677 |
. . . . . . . 8
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ (dom 𝑢 ∪ ran 𝑢)) |
81 | | funmpt 5964 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) |
82 | | resss 5457 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
83 | | dmss 5355 |
. . . . . . . . . 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} ‘𝑥)))) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
((𝑥 ∈ (On × On)
↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) ↾ 𝑢) ⊆ dom (𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) |
85 | | funimass3 6373 |
. . . . . . . . 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 𝑢)))) |
86 | 81, 84, 85 | mp2an 708 |
. . . . . . . 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 𝑢))) |
87 | 80, 86 | mpbir 221 |
. . . . . . 7
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ dom ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) ↾ 𝑢)) ⊆ (dom 𝑢 ∪ ran 𝑢) |
88 | 49, 87 | eqsstr3i 3669 |
. . . . . 6
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ⊆ (dom 𝑢 ∪ ran 𝑢) |
89 | 48, 88 | ssexi 4836 |
. . . . 5
⊢ ((𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V |
90 | 89 | a1i 11 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ (On
× On) ↦ ((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V) |
91 | 25, 39, 41, 44, 90 | fnwe 7338 |
. . 3
⊢ (⊤
→ 𝑅 We (On ×
On)) |
92 | | epse 5126 |
. . . . 5
⊢ E Se
On |
93 | 92 | a1i 11 |
. . . 4
⊢ (⊤
→ E Se On) |
94 | | vuniex 6996 |
. . . . . . . 8
⊢ ∪ 𝑢
∈ V |
95 | 94 | pwex 4878 |
. . . . . . 7
⊢ 𝒫
∪ 𝑢 ∈ V |
96 | 95, 95 | xpex 7004 |
. . . . . 6
⊢
(𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢)
∈ V |
97 | 5 | mptpreima 5666 |
. . . . . . . 8
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) = {𝑥 ∈ (On × On) ∣
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢} |
98 | | df-rab 2950 |
. . . . . . . 8
⊢ {𝑥 ∈ (On × On) ∣
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢} = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢)} |
99 | 97, 98 | eqtri 2673 |
. . . . . . 7
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) = {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢)} |
100 | 53 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
101 | | elssuni 4499 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑥) ∪ (2^{nd} ‘𝑥)) ∈ 𝑢 → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) ⊆ ∪ 𝑢) |
102 | 101 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → ((1^{st} ‘𝑥) ∪ (2^{nd}
‘𝑥)) ⊆ ∪ 𝑢) |
103 | 102 | unssad 3823 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (1^{st} ‘𝑥) ⊆ ∪ 𝑢) |
104 | 28 | elpw 4197 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (1^{st} ‘𝑥) ⊆ ∪ 𝑢) |
105 | 103, 104 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (1^{st} ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
106 | 102 | unssbd 3824 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (2^{nd} ‘𝑥) ⊆ ∪ 𝑢) |
107 | 30 | elpw 4197 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢
↔ (2^{nd} ‘𝑥) ⊆ ∪ 𝑢) |
108 | 106, 107 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → (2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢) |
109 | 105, 108 | jca 553 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → ((1^{st} ‘𝑥) ∈ 𝒫 ∪ 𝑢
∧ (2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢)) |
110 | | elxp6 7244 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) ↔ (𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩ ∧ ((1^{st}
‘𝑥) ∈ 𝒫
∪ 𝑢 ∧ (2^{nd} ‘𝑥) ∈ 𝒫 ∪ 𝑢))) |
111 | 100, 109,
110 | sylanbrc 699 |
. . . . . . . 8
⊢ ((𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢) → 𝑥 ∈ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢)) |
112 | 111 | abssi 3710 |
. . . . . . 7
⊢ {𝑥 ∣ (𝑥 ∈ (On × On) ∧
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥)) ∈ 𝑢)} ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
113 | 99, 112 | eqsstri 3668 |
. . . . . 6
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ⊆ (𝒫 ∪ 𝑢
× 𝒫 ∪ 𝑢) |
114 | 96, 113 | ssexi 4836 |
. . . . 5
⊢ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V |
115 | 114 | a1i 11 |
. . . 4
⊢ (⊤
→ (^{◡}(𝑥 ∈ (On × On) ↦
((1^{st} ‘𝑥)
∪ (2^{nd} ‘𝑥))) “ 𝑢) ∈ V) |
116 | 25, 39, 93, 115 | fnse 7339 |
. . 3
⊢ (⊤
→ 𝑅 Se (On ×
On)) |
117 | 91, 116 | jca 553 |
. 2
⊢ (⊤
→ (𝑅 We (On ×
On) ∧ 𝑅 Se (On ×
On))) |
118 | 117 | trud 1533 |
1
⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On ×
On)) |