Proof of Theorem r1val1
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) → 𝐴 = ∅) |
2 | 1 | fveq2d 6107 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) →
(𝑅1‘𝐴) =
(𝑅1‘∅)) |
3 | | r10 8514 |
. . . . 5
⊢
(𝑅1‘∅) = ∅ |
4 | 2, 3 | syl6eq 2660 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) →
(𝑅1‘𝐴) = ∅) |
5 | | 0ss 3924 |
. . . . 5
⊢ ∅
⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) → ∅ ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
7 | 4, 6 | eqsstrd 3602 |
. . 3
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = ∅) →
(𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
8 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑥 𝐴 ∈ dom
𝑅1 |
9 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥(𝑅1‘𝐴) |
10 | | nfiu1 4486 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) |
11 | 9, 10 | nfss 3561 |
. . . . 5
⊢
Ⅎ𝑥(𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) |
12 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝐴 = suc 𝑥) |
13 | 12 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘𝐴) =
(𝑅1‘suc 𝑥)) |
14 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝐴 = suc 𝑥 → (𝐴 ∈ dom 𝑅1 ↔ suc
𝑥 ∈ dom
𝑅1)) |
15 | 14 | biimpac 502 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → suc 𝑥 ∈ dom
𝑅1) |
16 | | r1funlim 8512 |
. . . . . . . . . . . . 13
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
17 | 16 | simpri 477 |
. . . . . . . . . . . 12
⊢ Lim dom
𝑅1 |
18 | | limsuc 6941 |
. . . . . . . . . . . 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 223 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝑥 ∈ dom
𝑅1) |
21 | | r1sucg 8515 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom
𝑅1 → (𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
23 | 13, 22 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘𝐴) = 𝒫
(𝑅1‘𝑥)) |
24 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
25 | 24 | sucid 5721 |
. . . . . . . . . 10
⊢ 𝑥 ∈ suc 𝑥 |
26 | 25, 12 | syl5eleqr 2695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝑥 ∈ 𝐴) |
27 | | ssiun2 4499 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → 𝒫
(𝑅1‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → 𝒫
(𝑅1‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
29 | 23, 28 | eqsstrd 3602 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝐴 = suc 𝑥) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
30 | 29 | ex 449 |
. . . . . 6
⊢ (𝐴 ∈ dom
𝑅1 → (𝐴 = suc 𝑥 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥))) |
31 | 30 | a1d 25 |
. . . . 5
⊢ (𝐴 ∈ dom
𝑅1 → (𝑥 ∈ On → (𝐴 = suc 𝑥 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)))) |
32 | 8, 11, 31 | rexlimd 3008 |
. . . 4
⊢ (𝐴 ∈ dom
𝑅1 → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥))) |
33 | 32 | imp 444 |
. . 3
⊢ ((𝐴 ∈ dom
𝑅1 ∧ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
34 | | r1limg 8517 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥)) |
35 | | r1tr 8522 |
. . . . . . . . 9
⊢ Tr
(𝑅1‘𝑥) |
36 | | dftr4 4685 |
. . . . . . . . 9
⊢ (Tr
(𝑅1‘𝑥) ↔ (𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥)) |
37 | 35, 36 | mpbi 219 |
. . . . . . . 8
⊢
(𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥) |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥)) |
39 | 38 | ralrimivw 2950 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥)) |
40 | | ss2iun 4472 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴
(𝑅1‘𝑥) ⊆ 𝒫
(𝑅1‘𝑥) → ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
42 | 34, 41 | eqsstrd 3602 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
43 | 42 | adantrl 748 |
. . 3
⊢ ((𝐴 ∈ dom
𝑅1 ∧ (𝐴 ∈ V ∧ Lim 𝐴)) → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
44 | | limord 5701 |
. . . . . . 7
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
45 | 17, 44 | ax-mp 5 |
. . . . . 6
⊢ Ord dom
𝑅1 |
46 | | ordsson 6881 |
. . . . . 6
⊢ (Ord dom
𝑅1 → dom 𝑅1 ⊆
On) |
47 | 45, 46 | ax-mp 5 |
. . . . 5
⊢ dom
𝑅1 ⊆ On |
48 | 47 | sseli 3564 |
. . . 4
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ∈ On) |
49 | | onzsl 6938 |
. . . 4
⊢ (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
50 | 48, 49 | sylib 207 |
. . 3
⊢ (𝐴 ∈ dom
𝑅1 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
51 | 7, 33, 43, 50 | mpjao3dan 1387 |
. 2
⊢ (𝐴 ∈ dom
𝑅1 → (𝑅1‘𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |
52 | | ordtr1 5684 |
. . . . . . . 8
⊢ (Ord dom
𝑅1 → ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1)) |
53 | 45, 52 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1) |
54 | 53 | ancoms 468 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom
𝑅1) |
55 | 54, 21 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
56 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
57 | | ordelord 5662 |
. . . . . . . . . 10
⊢ ((Ord dom
𝑅1 ∧ 𝐴 ∈ dom 𝑅1) →
Ord 𝐴) |
58 | 45, 57 | mpan 702 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom
𝑅1 → Ord 𝐴) |
59 | 58 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → Ord 𝐴) |
60 | | ordelsuc 6912 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ Ord 𝐴) → (𝑥 ∈ 𝐴 ↔ suc 𝑥 ⊆ 𝐴)) |
61 | 56, 59, 60 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↔ suc 𝑥 ⊆ 𝐴)) |
62 | 56, 61 | mpbid 221 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ⊆ 𝐴) |
63 | 54, 19 | sylib 207 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ dom
𝑅1) |
64 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ dom
𝑅1) |
65 | | r1ord3g 8525 |
. . . . . . 7
⊢ ((suc
𝑥 ∈ dom
𝑅1 ∧ 𝐴 ∈ dom 𝑅1) →
(suc 𝑥 ⊆ 𝐴 →
(𝑅1‘suc 𝑥) ⊆ (𝑅1‘𝐴))) |
66 | 63, 64, 65 | syl2anc 691 |
. . . . . 6
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ⊆ 𝐴 → (𝑅1‘suc
𝑥) ⊆
(𝑅1‘𝐴))) |
67 | 62, 66 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → (𝑅1‘suc
𝑥) ⊆
(𝑅1‘𝐴)) |
68 | 55, 67 | eqsstr3d 3603 |
. . . 4
⊢ ((𝐴 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐴) → 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
69 | 68 | ralrimiva 2949 |
. . 3
⊢ (𝐴 ∈ dom
𝑅1 → ∀𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
70 | | iunss 4497 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴) ↔ ∀𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
71 | 69, 70 | sylibr 223 |
. 2
⊢ (𝐴 ∈ dom
𝑅1 → ∪ 𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥) ⊆ (𝑅1‘𝐴)) |
72 | 51, 71 | eqssd 3585 |
1
⊢ (𝐴 ∈ dom
𝑅1 → (𝑅1‘𝐴) = ∪
𝑥 ∈ 𝐴 𝒫
(𝑅1‘𝑥)) |