| Step | Hyp | Ref
| Expression |
| 1 | | gruina.1 |
. . . . . 6
⊢ 𝐴 = (𝑈 ∩ On) |
| 2 | | inss1 4237 |
. . . . . 6
⊢ (𝑈 ∩ On) ⊆ 𝑈 |
| 3 | 1, 2 | eqsstri 4030 |
. . . . 5
⊢ 𝐴 ⊆ 𝑈 |
| 4 | | sseq2 4010 |
. . . . 5
⊢ (𝑈 = ∅ → (𝐴 ⊆ 𝑈 ↔ 𝐴 ⊆ ∅)) |
| 5 | 3, 4 | mpbii 233 |
. . . 4
⊢ (𝑈 = ∅ → 𝐴 ⊆
∅) |
| 6 | | ss0 4402 |
. . . 4
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
| 7 | | fveq2 6906 |
. . . . . 6
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) =
(𝑅1‘∅)) |
| 8 | | r10 9808 |
. . . . . 6
⊢
(𝑅1‘∅) = ∅ |
| 9 | 7, 8 | eqtrdi 2793 |
. . . . 5
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) = ∅) |
| 10 | | 0ss 4400 |
. . . . 5
⊢ ∅
⊆ 𝑈 |
| 11 | 9, 10 | eqsstrdi 4028 |
. . . 4
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) ⊆ 𝑈) |
| 12 | 5, 6, 11 | 3syl 18 |
. . 3
⊢ (𝑈 = ∅ →
(𝑅1‘𝐴) ⊆ 𝑈) |
| 13 | 12 | a1i 11 |
. 2
⊢ (𝑈 ∈ Univ → (𝑈 = ∅ →
(𝑅1‘𝐴) ⊆ 𝑈)) |
| 14 | 1 | gruina 10858 |
. . . . 5
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc) |
| 15 | | inawina 10730 |
. . . . 5
⊢ (𝐴 ∈ Inacc → 𝐴 ∈
Inaccw) |
| 16 | | winaon 10728 |
. . . . . 6
⊢ (𝐴 ∈ Inaccw →
𝐴 ∈
On) |
| 17 | | winalim 10735 |
. . . . . 6
⊢ (𝐴 ∈ Inaccw →
Lim 𝐴) |
| 18 | | r1lim 9812 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) →
(𝑅1‘𝐴) = ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥)) |
| 19 | 16, 17, 18 | syl2anc 584 |
. . . . 5
⊢ (𝐴 ∈ Inaccw →
(𝑅1‘𝐴) = ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥)) |
| 20 | 14, 15, 19 | 3syl 18 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(𝑅1‘𝐴) = ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥)) |
| 21 | | inss2 4238 |
. . . . . . . . . . . 12
⊢ (𝑈 ∩ On) ⊆
On |
| 22 | 1, 21 | eqsstri 4030 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ On |
| 23 | 22 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ On) |
| 24 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
| 25 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) =
(𝑅1‘∅)) |
| 26 | 25, 8 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) = ∅) |
| 27 | 26 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ →
((𝑅1‘𝑥) ∈ 𝑈 ↔ ∅ ∈ 𝑈)) |
| 28 | 24, 27 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ∈ 𝑈) ↔ (∅ ∈ 𝐴 → ∅ ∈ 𝑈))) |
| 29 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
| 30 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
| 31 | 30 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ∈ 𝑈 ↔ (𝑅1‘𝑦) ∈ 𝑈)) |
| 32 | 29, 31 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ∈ 𝑈) ↔ (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈))) |
| 33 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴)) |
| 34 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
| 35 | 34 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ∈ 𝑈 ↔ (𝑅1‘suc
𝑦) ∈ 𝑈)) |
| 36 | 33, 35 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ∈ 𝑈) ↔ (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc
𝑦) ∈ 𝑈))) |
| 37 | 3 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (∅
∈ 𝐴 → ∅
∈ 𝑈) |
| 38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ Univ → (∅
∈ 𝐴 → ∅
∈ 𝑈)) |
| 39 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → suc 𝑦 ∈ 𝐴) |
| 40 | | elelsuc 6457 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑦 ∈ 𝐴 → suc 𝑦 ∈ suc 𝐴) |
| 41 | 3 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (suc
𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝑈) |
| 42 | 41 | ne0d 4342 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑦 ∈ 𝐴 → 𝑈 ≠ ∅) |
| 43 | 14, 15, 16 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ On) |
| 44 | 42, 43 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → 𝐴 ∈ On) |
| 45 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 46 | | ordsucelsuc 7842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝐴 → (𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ suc 𝐴)) |
| 47 | 44, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝐴 ↔ suc 𝑦 ∈ suc 𝐴)) |
| 48 | 40, 47 | imbitrrid 246 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
| 49 | 39, 48 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 50 | | grupw 10835 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧
(𝑅1‘𝑦) ∈ 𝑈) → 𝒫
(𝑅1‘𝑦) ∈ 𝑈) |
| 51 | 50 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ Univ →
((𝑅1‘𝑦) ∈ 𝑈 → 𝒫
(𝑅1‘𝑦) ∈ 𝑈)) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → ((𝑅1‘𝑦) ∈ 𝑈 → 𝒫
(𝑅1‘𝑦) ∈ 𝑈)) |
| 53 | | r1suc 9810 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ On →
(𝑅1‘suc 𝑦) = 𝒫
(𝑅1‘𝑦)) |
| 54 | 53 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ On →
((𝑅1‘suc 𝑦) ∈ 𝑈 ↔ 𝒫
(𝑅1‘𝑦) ∈ 𝑈)) |
| 55 | 54 | biimprcd 250 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 (𝑅1‘𝑦) ∈ 𝑈 → (𝑦 ∈ On →
(𝑅1‘suc 𝑦) ∈ 𝑈)) |
| 56 | 52, 55 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → ((𝑅1‘𝑦) ∈ 𝑈 → (𝑦 ∈ On →
(𝑅1‘suc 𝑦) ∈ 𝑈))) |
| 57 | 49, 56 | embantd 59 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ Univ ∧ suc 𝑦 ∈ 𝐴) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑦 ∈ On →
(𝑅1‘suc 𝑦) ∈ 𝑈))) |
| 58 | 57 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ Univ → (suc 𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑦 ∈ On →
(𝑅1‘suc 𝑦) ∈ 𝑈)))) |
| 59 | 58 | com23 86 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ Univ → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (suc 𝑦 ∈ 𝐴 → (𝑦 ∈ On →
(𝑅1‘suc 𝑦) ∈ 𝑈)))) |
| 60 | 59 | com4r 94 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On → (𝑈 ∈ Univ → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc
𝑦) ∈ 𝑈)))) |
| 61 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 62 | 3 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈) |
| 63 | 62 | ne0d 4342 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 → 𝑈 ≠ ∅) |
| 64 | 63, 43 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ On) |
| 65 | | ontr1 6430 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
| 66 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑦) ∈ 𝑈)) |
| 67 | 65, 66 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑦) ∈ 𝑈))) |
| 68 | 67 | expd 415 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑦) ∈ 𝑈)))) |
| 69 | 68 | com3r 87 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → (𝐴 ∈ On → (𝑦 ∈ 𝑥 → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑦) ∈ 𝑈)))) |
| 70 | 61, 64, 69 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑦) ∈ 𝑈))) |
| 71 | 70 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑦) ∈ 𝑈)) |
| 72 | 71 | ralimdva 3167 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → ∀𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈)) |
| 73 | | gruiun 10839 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈) → ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈) |
| 74 | 73 | 3expia 1122 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (∀𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈 → ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈)) |
| 75 | 62, 74 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈 → ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈)) |
| 76 | 72, 75 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈)) |
| 77 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
| 78 | | r1lim 9812 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) →
(𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) |
| 79 | 77, 78 | mpan 690 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝑥 →
(𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) |
| 80 | 79 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑥 →
((𝑅1‘𝑥) ∈ 𝑈 ↔ ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈)) |
| 81 | 80 | biimprd 248 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝑥 → (∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝑈 → (𝑅1‘𝑥) ∈ 𝑈)) |
| 82 | 76, 81 | sylan9r 508 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝑥 ∧ (𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴)) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑥) ∈ 𝑈)) |
| 83 | 82 | exp32 420 |
. . . . . . . . . . . . 13
⊢ (Lim
𝑥 → (𝑈 ∈ Univ → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑅1‘𝑥) ∈ 𝑈)))) |
| 84 | 83 | com34 91 |
. . . . . . . . . . . 12
⊢ (Lim
𝑥 → (𝑈 ∈ Univ → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ∈ 𝑈) → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ∈ 𝑈)))) |
| 85 | 28, 32, 36, 38, 60, 84 | tfinds2 7885 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → (𝑈 ∈ Univ → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ∈ 𝑈))) |
| 86 | 85 | com3r 87 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ On → (𝑈 ∈ Univ →
(𝑅1‘𝑥) ∈ 𝑈))) |
| 87 | 23, 86 | mpd 15 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (𝑈 ∈ Univ →
(𝑅1‘𝑥) ∈ 𝑈)) |
| 88 | 87 | impcom 407 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ∈ 𝑈) |
| 89 | | gruelss 10834 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧
(𝑅1‘𝑥) ∈ 𝑈) → (𝑅1‘𝑥) ⊆ 𝑈) |
| 90 | 88, 89 | syldan 591 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ⊆ 𝑈) |
| 91 | 90 | ralrimiva 3146 |
. . . . . 6
⊢ (𝑈 ∈ Univ →
∀𝑥 ∈ 𝐴
(𝑅1‘𝑥) ⊆ 𝑈) |
| 92 | | iunss 5045 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ 𝑈 ↔ ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ 𝑈) |
| 93 | 91, 92 | sylibr 234 |
. . . . 5
⊢ (𝑈 ∈ Univ → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ 𝑈) |
| 94 | 93 | adantr 480 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ⊆ 𝑈) |
| 95 | 20, 94 | eqsstrd 4018 |
. . 3
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) →
(𝑅1‘𝐴) ⊆ 𝑈) |
| 96 | 95 | ex 412 |
. 2
⊢ (𝑈 ∈ Univ → (𝑈 ≠ ∅ →
(𝑅1‘𝐴) ⊆ 𝑈)) |
| 97 | 13, 96 | pm2.61dne 3028 |
1
⊢ (𝑈 ∈ Univ →
(𝑅1‘𝐴) ⊆ 𝑈) |