Proof of Theorem r1val1
Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) → 𝐴 = ∅) |
2 | 1 | fveq2d 6678 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) →
(𝑅1‘𝐴) =
(𝑅1‘∅)) |
3 | | r10 9270 |
. . . . 5
⊢
(𝑅1‘∅) = ∅ |
4 | 2, 3 | eqtrdi 2789 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) →
(𝑅1‘𝐴) = ∅) |
5 | | 0ss 4285 |
. . . . 5
⊢ ∅
⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) → ∅ ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
7 | 4, 6 | eqsstrd 3915 |
. . 3
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) →
(𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
8 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑥 𝐴 ∈ dom
𝑅1 |
9 | | nfcv 2899 |
. . . . . 6
⊢
Ⅎ𝑥(𝑅1‘𝐴) |
10 | | nfiu1 4915 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) |
11 | 9, 10 | nfss 3869 |
. . . . 5
⊢
Ⅎ𝑥(𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) |
12 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝐴 = suc 𝑥) |
13 | 12 | fveq2d 6678 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘𝐴) =
(𝑅1‘suc 𝑥)) |
14 | | eleq1 2820 |
. . . . . . . . . . . 12
⊢ (𝐴 = suc 𝑥 → (𝐴 ∈ dom 𝑅1 ↔ suc
𝑥 ∈ dom
𝑅1)) |
15 | 14 | biimpac 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → suc 𝑥 ∈ dom
𝑅1) |
16 | | r1funlim 9268 |
. . . . . . . . . . . . 13
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
17 | 16 | simpri 489 |
. . . . . . . . . . . 12
⊢ Lim dom
𝑅1 |
18 | | limsuc 7583 |
. . . . . . . . . . . 12
⊢ (Lim dom
𝑅1 → (𝑥 ∈ dom 𝑅1 ↔ suc
𝑥 ∈ dom
𝑅1)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ dom
𝑅1 ↔ suc 𝑥 ∈ dom
𝑅1) |
20 | 15, 19 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝑥 ∈ dom
𝑅1) |
21 | | r1sucg 9271 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom
𝑅1 → (𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
23 | 13, 22 | eqtrd 2773 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘𝐴) = 𝒫
(𝑅1‘𝑥)) |
24 | | vex 3402 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
25 | 24 | sucid 6251 |
. . . . . . . . . 10
⊢ 𝑥 ∈ suc 𝑥 |
26 | 25, 12 | eleqtrrid 2840 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝑥 ∈ 𝐴) |
27 | | ssiun2 4933 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → 𝒫
(𝑅1‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝒫
(𝑅1‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
29 | 23, 28 | eqsstrd 3915 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
30 | 29 | ex 416 |
. . . . . 6
⊢ (𝐴 ∈ dom
𝑅1 → (𝐴 = suc 𝑥 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥))) |
31 | 30 | a1d 25 |
. . . . 5
⊢ (𝐴 ∈ dom
𝑅1 → (𝑥 ∈ On → (𝐴 = suc 𝑥 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)))) |
32 | 8, 11, 31 | rexlimd 3227 |
. . . 4
⊢ (𝐴 ∈ dom
𝑅1 → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥))) |
33 | 32 | imp 410 |
. . 3
⊢ ((𝐴 ∈ dom
𝑅1 ∧ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
34 | | r1limg 9273 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥)) |
35 | | r1tr 9278 |
. . . . . . . . 9
⊢ Tr
(𝑅1‘𝑥) |
36 | | dftr4 5141 |
. . . . . . . . 9
⊢ (Tr
(𝑅1‘𝑥) ↔ (𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥)) |
37 | 35, 36 | mpbi 233 |
. . . . . . . 8
⊢
(𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥) |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥)) |
39 | 38 | ralrimivw 3097 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥)) |
40 | | ss2iun 4899 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴
(𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥) → ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
42 | 34, 41 | eqsstrd 3915 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
43 | 42 | adantrl 716 |
. . 3
⊢ ((𝐴 ∈ dom
𝑅1 ∧ (𝐴 ∈ V ∧ Lim 𝐴)) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
44 | | limord 6231 |
. . . . . . 7
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
45 | 17, 44 | ax-mp 5 |
. . . . . 6
⊢ Ord dom
𝑅1 |
46 | | ordsson 7523 |
. . . . . 6
⊢ (Ord dom
𝑅1 → dom 𝑅1 ⊆
On) |
47 | 45, 46 | ax-mp 5 |
. . . . 5
⊢ dom
𝑅1 ⊆ On |
48 | 47 | sseli 3873 |
. . . 4
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ∈ On) |
49 | | onzsl 7580 |
. . . 4
⊢ (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
50 | 48, 49 | sylib 221 |
. . 3
⊢ (𝐴 ∈ dom
𝑅1 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
51 | 7, 33, 43, 50 | mpjao3dan 1432 |
. 2
⊢ (𝐴 ∈ dom
𝑅1 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
52 | | ordtr1 6215 |
. . . . . . . 8
⊢ (Ord dom
𝑅1 → ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1)) |
53 | 45, 52 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1) |
54 | 53 | ancoms 462 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom
𝑅1) |
55 | 54, 21 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
56 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
57 | | ordelord 6194 |
. . . . . . . . . 10
⊢ ((Ord dom
𝑅1 ∧ 𝐴 ∈ dom 𝑅1) →
Ord 𝐴) |
58 | 45, 57 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom
𝑅1 → Ord 𝐴) |
59 | 58 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → Ord 𝐴) |
60 | | ordelsuc 7554 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ Ord 𝐴) → (𝑥 ∈ 𝐴 ↔ suc 𝑥 ⊆ 𝐴)) |
61 | 56, 59, 60 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↔ suc 𝑥 ⊆ 𝐴)) |
62 | 56, 61 | mpbid 235 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ⊆ 𝐴) |
63 | 54, 19 | sylib 221 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ dom
𝑅1) |
64 | | simpl 486 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ dom
𝑅1) |
65 | | r1ord3g 9281 |
. . . . . . 7
⊢ ((suc
𝑥 ∈ dom
𝑅1 ∧ 𝐴 ∈ dom 𝑅1) →
(suc 𝑥 ⊆ 𝐴 →
(𝑅1‘suc 𝑥) ⊆ (𝑅1‘𝐴))) |
66 | 63, 64, 65 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ⊆ 𝐴 → (𝑅1‘suc
𝑥) ⊆
(𝑅1‘𝐴))) |
67 | 62, 66 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (𝑅1‘suc
𝑥) ⊆
(𝑅1‘𝐴)) |
68 | 55, 67 | eqsstrrd 3916 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
69 | 68 | ralrimiva 3096 |
. . 3
⊢ (𝐴 ∈ dom
𝑅1 → ∀𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
70 | | iunss 4931 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴) ↔ ∀𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
71 | 69, 70 | sylibr 237 |
. 2
⊢ (𝐴 ∈ dom
𝑅1 → ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
72 | 51, 71 | eqssd 3894 |
1
⊢ (𝐴 ∈ dom
𝑅1 → (𝑅1‘𝐴) = ∪
𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |