| Step | Hyp | Ref
| Expression |
| 1 | | inawina 10730 |
. . . . . 6
⊢ (𝐴 ∈ Inacc → 𝐴 ∈
Inaccw) |
| 2 | | winaon 10728 |
. . . . . 6
⊢ (𝐴 ∈ Inaccw →
𝐴 ∈
On) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Inacc → 𝐴 ∈ On) |
| 4 | | winalim 10735 |
. . . . . 6
⊢ (𝐴 ∈ Inaccw →
Lim 𝐴) |
| 5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Inacc → Lim 𝐴) |
| 6 | | r1lim 9812 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) →
(𝑅1‘𝐴) = ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥)) |
| 7 | 3, 5, 6 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) = ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥)) |
| 8 | | onelon 6409 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
| 9 | 3, 8 | sylan 580 |
. . . . . . . 8
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
| 10 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
| 11 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) =
(𝑅1‘∅)) |
| 12 | 11 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
((𝑅1‘𝑥) ≺ 𝐴 ↔
(𝑅1‘∅) ≺ 𝐴)) |
| 13 | 10, 12 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (∅ ∈ 𝐴 →
(𝑅1‘∅) ≺ 𝐴))) |
| 14 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
| 15 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
| 16 | 15 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴)) |
| 17 | 14, 16 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) |
| 18 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴)) |
| 19 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
| 20 | 19 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ≺ 𝐴 ↔ (𝑅1‘suc
𝑦) ≺ 𝐴)) |
| 21 | 18, 20 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴) ↔ (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc
𝑦) ≺ 𝐴))) |
| 22 | | ne0i 4341 |
. . . . . . . . . . . . 13
⊢ (∅
∈ 𝐴 → 𝐴 ≠ ∅) |
| 23 | | 0sdomg 9144 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 24 | 22, 23 | imbitrrid 246 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 → ∅
≺ 𝐴)) |
| 25 | | r10 9808 |
. . . . . . . . . . . . 13
⊢
(𝑅1‘∅) = ∅ |
| 26 | 25 | breq1i 5150 |
. . . . . . . . . . . 12
⊢
((𝑅1‘∅) ≺ 𝐴 ↔ ∅ ≺ 𝐴) |
| 27 | 24, 26 | imbitrrdi 252 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 →
(𝑅1‘∅) ≺ 𝐴)) |
| 28 | 1, 2, 27 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Inacc → (∅
∈ 𝐴 →
(𝑅1‘∅) ≺ 𝐴)) |
| 29 | | eloni 6394 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 30 | | ordtr 6398 |
. . . . . . . . . . . . . . 15
⊢ (Ord
𝐴 → Tr 𝐴) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → Tr 𝐴) |
| 32 | | trsuc 6471 |
. . . . . . . . . . . . . . 15
⊢ ((Tr
𝐴 ∧ suc 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 33 | 32 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (Tr 𝐴 → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
| 34 | 3, 31, 33 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Inacc → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → (suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
| 36 | | r1suc 9810 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ On →
(𝑅1‘suc 𝑦) = 𝒫
(𝑅1‘𝑦)) |
| 37 | | fvex 6919 |
. . . . . . . . . . . . . . . . . 18
⊢
(𝑅1‘𝑦) ∈ V |
| 38 | 37 | cardid 10587 |
. . . . . . . . . . . . . . . . 17
⊢
(card‘(𝑅1‘𝑦)) ≈ (𝑅1‘𝑦) |
| 39 | 38 | ensymi 9044 |
. . . . . . . . . . . . . . . 16
⊢
(𝑅1‘𝑦) ≈
(card‘(𝑅1‘𝑦)) |
| 40 | | pwen 9190 |
. . . . . . . . . . . . . . . 16
⊢
((𝑅1‘𝑦) ≈
(card‘(𝑅1‘𝑦)) → 𝒫
(𝑅1‘𝑦) ≈ 𝒫
(card‘(𝑅1‘𝑦))) |
| 41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
(𝑅1‘𝑦) ≈ 𝒫
(card‘(𝑅1‘𝑦)) |
| 42 | 36, 41 | eqbrtrdi 5182 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ On →
(𝑅1‘suc 𝑦) ≈ 𝒫
(card‘(𝑅1‘𝑦))) |
| 43 | | winacard 10732 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Inaccw →
(card‘𝐴) = 𝐴) |
| 44 | 43 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ Inaccw →
((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔
(card‘(𝑅1‘𝑦)) ∈ 𝐴)) |
| 45 | | cardsdom 10595 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((𝑅1‘𝑦) ∈ V ∧ 𝐴 ∈ On) →
((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴)) |
| 46 | 37, 2, 45 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ Inaccw →
((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴)) |
| 47 | 44, 46 | bitr3d 281 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Inaccw →
((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴)) |
| 48 | 1, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Inacc →
((card‘(𝑅1‘𝑦)) ∈ 𝐴 ↔ (𝑅1‘𝑦) ≺ 𝐴)) |
| 49 | | elina 10727 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧
(cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴)) |
| 50 | 49 | simp3bi 1148 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Inacc →
∀𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴) |
| 51 | | pweq 4614 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 =
(card‘(𝑅1‘𝑦)) → 𝒫 𝑧 = 𝒫
(card‘(𝑅1‘𝑦))) |
| 52 | 51 | breq1d 5153 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 =
(card‘(𝑅1‘𝑦)) → (𝒫 𝑧 ≺ 𝐴 ↔ 𝒫
(card‘(𝑅1‘𝑦)) ≺ 𝐴)) |
| 53 | 52 | rspccv 3619 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
𝐴 𝒫 𝑧 ≺ 𝐴 →
((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫
(card‘(𝑅1‘𝑦)) ≺ 𝐴)) |
| 54 | 50, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Inacc →
((card‘(𝑅1‘𝑦)) ∈ 𝐴 → 𝒫
(card‘(𝑅1‘𝑦)) ≺ 𝐴)) |
| 55 | 48, 54 | sylbird 260 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Inacc →
((𝑅1‘𝑦) ≺ 𝐴 → 𝒫
(card‘(𝑅1‘𝑦)) ≺ 𝐴)) |
| 56 | 55 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Inacc ∧
(𝑅1‘𝑦) ≺ 𝐴) → 𝒫
(card‘(𝑅1‘𝑦)) ≺ 𝐴) |
| 57 | | ensdomtr 9153 |
. . . . . . . . . . . . . 14
⊢
(((𝑅1‘suc 𝑦) ≈ 𝒫
(card‘(𝑅1‘𝑦)) ∧ 𝒫
(card‘(𝑅1‘𝑦)) ≺ 𝐴) → (𝑅1‘suc
𝑦) ≺ 𝐴) |
| 58 | 42, 56, 57 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ (𝐴 ∈ Inacc ∧
(𝑅1‘𝑦) ≺ 𝐴)) → (𝑅1‘suc
𝑦) ≺ 𝐴) |
| 59 | 58 | expr 456 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) →
((𝑅1‘𝑦) ≺ 𝐴 → (𝑅1‘suc
𝑦) ≺ 𝐴)) |
| 60 | 35, 59 | imim12d 81 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ Inacc) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc
𝑦) ≺ 𝐴))) |
| 61 | 60 | ex 412 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → (𝐴 ∈ Inacc → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (suc 𝑦 ∈ 𝐴 → (𝑅1‘suc
𝑦) ≺ 𝐴)))) |
| 62 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
| 63 | | r1lim 9812 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) →
(𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧)) |
| 64 | 62, 63 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝑥 →
(𝑅1‘𝑥) = ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧)) |
| 65 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦𝑧 |
| 66 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦(𝑅1‘𝑧) |
| 67 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦
≼ |
| 68 | | nfiu1 5027 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) |
| 69 | 66, 67, 68 | nfbr 5190 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦(𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) |
| 70 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → (𝑅1‘𝑦) =
(𝑅1‘𝑧)) |
| 71 | 70 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → ((𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ↔ (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 72 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(card‘(𝑅1‘𝑦)) ∈ V |
| 73 | 62, 72 | iunex 7993 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ V |
| 74 | | ssiun2 5047 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝑥 →
(card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 75 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ V →
((card‘(𝑅1‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) →
(card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 76 | 73, 74, 75 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑥 →
(card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 77 | | endomtr 9052 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((𝑅1‘𝑦) ≈
(card‘(𝑅1‘𝑦)) ∧
(card‘(𝑅1‘𝑦)) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 78 | 39, 76, 77 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 79 | 65, 69, 71, 78 | vtoclgaf 3576 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑥 → (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 80 | 79 | rgen 3063 |
. . . . . . . . . . . . . . . . 17
⊢
∀𝑧 ∈
𝑥
(𝑅1‘𝑧) ≼ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) |
| 81 | | iundom 10582 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ V ∧ ∀𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 82 | 62, 80, 81 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 83 | 62, 73 | unex 7764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ V |
| 84 | | ssun2 4179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 85 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ V → (∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ⊆ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 86 | 83, 84, 85 | mp2 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 87 | 62 | xpdom2 9107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝑥 × ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 89 | | ssun1 4178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ⊆ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 90 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ V → (𝑥 ⊆ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → 𝑥 ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 91 | 83, 89, 90 | mp2 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 92 | 83 | xpdom1 9111 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝑥 × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 93 | 91, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 94 | | domtr 9047 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ (𝑥 × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ∧ (𝑥 × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ≼ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) → (𝑥 × ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 95 | 88, 93, 94 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 × ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 96 | | limomss 7892 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
𝑥 → ω ⊆
𝑥) |
| 97 | 96, 89 | sstrdi 3996 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
𝑥 → ω ⊆
(𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 98 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ V → (ω ⊆ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → ω ≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 99 | 83, 97, 98 | mpsyl 68 |
. . . . . . . . . . . . . . . . . 18
⊢ (Lim
𝑥 → ω ≼
(𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 100 | | infxpidm 10602 |
. . . . . . . . . . . . . . . . . 18
⊢ (ω
≼ (𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝑥 → ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 102 | | domentr 9053 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 × ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ∧ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) × (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) ≈ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) → (𝑥 × ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 103 | 95, 101, 102 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑥 → (𝑥 × ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 104 | | domtr 9047 |
. . . . . . . . . . . . . . . 16
⊢
((∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 × ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∧ (𝑥 × ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 105 | 82, 103, 104 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝑥 → ∪ 𝑧 ∈ 𝑥 (𝑅1‘𝑧) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 106 | 64, 105 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ (Lim
𝑥 →
(𝑅1‘𝑥) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 107 | 106 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) →
(𝑅1‘𝑥) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 108 | | eleq1a 2836 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → (𝐴 = 𝑥 → 𝐴 ∈ 𝐴)) |
| 109 | | ordirr 6402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Ord
𝐴 → ¬ 𝐴 ∈ 𝐴) |
| 110 | 3, 29, 109 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Inacc → ¬ 𝐴 ∈ 𝐴) |
| 111 | 108, 110 | nsyli 157 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐴 → (𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥)) |
| 112 | 111 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Inacc) → ¬ 𝐴 = 𝑥) |
| 113 | 112 | ad2ant2r 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = 𝑥) |
| 114 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ 𝐴) |
| 115 | | limord 6444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Lim
𝑥 → Ord 𝑥) |
| 116 | 62 | elon 6393 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ On ↔ Ord 𝑥) |
| 117 | 115, 116 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
| 118 | 117 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ∈ On) |
| 119 | | cardf 10590 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
card:V⟶On |
| 120 | | r1fnon 9807 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
𝑅1 Fn On |
| 121 | | dffn2 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(𝑅1 Fn On ↔
𝑅1:On⟶V) |
| 122 | 120, 121 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
𝑅1:On⟶V |
| 123 | | fco 6760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((card:V⟶On ∧ 𝑅1:On⟶V) → (card
∘ 𝑅1):On⟶On) |
| 124 | 119, 122,
123 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (card
∘ 𝑅1):On⟶On |
| 125 | | onss 7805 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
| 126 | | fssres 6774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((card
∘ 𝑅1):On⟶On ∧ 𝑥 ⊆ On) → ((card ∘
𝑅1) ↾ 𝑥):𝑥⟶On) |
| 127 | 124, 125,
126 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ On → ((card ∘
𝑅1) ↾ 𝑥):𝑥⟶On) |
| 128 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((card
∘ 𝑅1) ↾ 𝑥):𝑥⟶On → ((card ∘
𝑅1) ↾ 𝑥) Fn 𝑥) |
| 129 | 118, 127,
128 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘
𝑅1) ↾ 𝑥) Fn 𝑥) |
| 130 | 3 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On) |
| 131 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
| 132 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝐴) |
| 133 | | ontr1 6430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
| 134 | 133 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
| 135 | 130, 131,
132, 134 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
| 136 | 37, 130, 45 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) →
((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔ (𝑅1‘𝑦) ≺ 𝐴)) |
| 137 | 1, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐴 ∈ Inacc →
(card‘𝐴) = 𝐴) |
| 138 | 137 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (card‘𝐴) = 𝐴) |
| 139 | 138 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) →
((card‘(𝑅1‘𝑦)) ∈ (card‘𝐴) ↔
(card‘(𝑅1‘𝑦)) ∈ 𝐴)) |
| 140 | 136, 139 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 ↔
(card‘(𝑅1‘𝑦)) ∈ 𝐴)) |
| 141 | 140 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑦) ≺ 𝐴 →
(card‘(𝑅1‘𝑦)) ∈ 𝐴)) |
| 142 | 135, 141 | embantd 59 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) →
(card‘(𝑅1‘𝑦)) ∈ 𝐴)) |
| 143 | 117 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → 𝑥 ∈ On) |
| 144 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ 𝑥 → (((card ∘
𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘
𝑅1)‘𝑦)) |
| 145 | 144 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘
𝑅1) ↾ 𝑥)‘𝑦) = ((card ∘
𝑅1)‘𝑦)) |
| 146 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
| 147 | | fvco3 7008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((𝑅1:On⟶V ∧ 𝑦 ∈ On) → ((card ∘
𝑅1)‘𝑦) =
(card‘(𝑅1‘𝑦))) |
| 148 | 122, 146,
147 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((card ∘
𝑅1)‘𝑦) =
(card‘(𝑅1‘𝑦))) |
| 149 | 145, 148 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (((card ∘
𝑅1) ↾ 𝑥)‘𝑦) =
(card‘(𝑅1‘𝑦))) |
| 150 | 143, 149 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → (((card ∘
𝑅1) ↾ 𝑥)‘𝑦) =
(card‘(𝑅1‘𝑦))) |
| 151 | 150 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((((card ∘
𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴 ↔
(card‘(𝑅1‘𝑦)) ∈ 𝐴)) |
| 152 | 142, 151 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (((card ∘
𝑅1) ↾ 𝑥)‘𝑦) ∈ 𝐴)) |
| 153 | 152 | ralimdva 3167 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1)
↾ 𝑥)‘𝑦) ∈ 𝐴)) |
| 154 | 153 | impr 454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1)
↾ 𝑥)‘𝑦) ∈ 𝐴) |
| 155 | | ffnfv 7139 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((card
∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ↔ (((card ∘
𝑅1) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (((card ∘ 𝑅1)
↾ 𝑥)‘𝑦) ∈ 𝐴)) |
| 156 | 129, 154,
155 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((card ∘
𝑅1) ↾ 𝑥):𝑥⟶𝐴) |
| 157 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 158 | 157 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 159 | | eliun 4995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑧 ∈
(card‘(𝑅1‘𝑦))) |
| 160 | | cardon 9984 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(card‘(𝑅1‘𝑦)) ∈ On |
| 161 | 160 | onelssi 6499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈
(card‘(𝑅1‘𝑦)) → 𝑧 ⊆
(card‘(𝑅1‘𝑦))) |
| 162 | 149 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦) ↔ 𝑧 ⊆
(card‘(𝑅1‘𝑦)))) |
| 163 | 161, 162 | imbitrrid 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈
(card‘(𝑅1‘𝑦)) → 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 164 | 163 | reximdva 3168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 𝑧 ∈
(card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 165 | 159, 164 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ On → (𝑧 ∈ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 166 | 158, 165 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ On → ((𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 167 | 166 | expdimp 452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 168 | 167 | ralrimiv 3145 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦)) |
| 169 | 168 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ On → (𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 170 | 118, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 171 | | ffun 6739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((card
∘ 𝑅1):On⟶On → Fun (card ∘
𝑅1)) |
| 172 | 124, 171 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Fun (card
∘ 𝑅1) |
| 173 | | resfunexg 7235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
(card ∘ 𝑅1) ∧ 𝑥 ∈ V) → ((card ∘
𝑅1) ↾ 𝑥) ∈ V) |
| 174 | 172, 62, 173 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((card
∘ 𝑅1) ↾ 𝑥) ∈ V |
| 175 | | feq1 6716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = ((card ∘
𝑅1) ↾ 𝑥) → (𝑤:𝑥⟶𝐴 ↔ ((card ∘
𝑅1) ↾ 𝑥):𝑥⟶𝐴)) |
| 176 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = ((card ∘
𝑅1) ↾ 𝑥) → (𝑤‘𝑦) = (((card ∘ 𝑅1)
↾ 𝑥)‘𝑦)) |
| 177 | 176 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = ((card ∘
𝑅1) ↾ 𝑥) → (𝑧 ⊆ (𝑤‘𝑦) ↔ 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 178 | 177 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = ((card ∘
𝑅1) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 179 | 178 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = ((card ∘
𝑅1) ↾ 𝑥) → (∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦))) |
| 180 | 175, 179 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = ((card ∘
𝑅1) ↾ 𝑥) → ((𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) ↔ (((card ∘
𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦)))) |
| 181 | 174, 180 | spcev 3606 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((card
∘ 𝑅1) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (((card ∘
𝑅1) ↾ 𝑥)‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦))) |
| 182 | 156, 170,
181 | syl6an 684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → ∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)))) |
| 183 | 3 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝐴 ∈ On) |
| 184 | | cfflb 10299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥)) |
| 185 | 183, 118,
184 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (∃𝑤(𝑤:𝑥⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝑤‘𝑦)) → (cf‘𝐴) ⊆ 𝑥)) |
| 186 | 182, 185 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → (cf‘𝐴) ⊆ 𝑥)) |
| 187 | 49 | simp2bi 1147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ Inacc →
(cf‘𝐴) = 𝐴) |
| 188 | 187 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ Inacc →
((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥)) |
| 189 | 188 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((cf‘𝐴) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥)) |
| 190 | 186, 189 | sylibd 239 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → 𝐴 ⊆ 𝑥)) |
| 191 | | ontri1 6418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴)) |
| 192 | 183, 118,
191 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴)) |
| 193 | 190, 192 | sylibd 239 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) → ¬ 𝑥 ∈ 𝐴)) |
| 194 | 114, 193 | mt2d 136 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ 𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 195 | | iunon 8379 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ On) |
| 196 | 62, 195 | mpan 690 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑦 ∈
𝑥
(card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ On) |
| 197 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑥 →
(card‘(𝑅1‘𝑦)) ∈ On) |
| 198 | 196, 197 | mprg 3067 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ On |
| 199 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴 ↔ 𝐴 = (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)))) |
| 200 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → Ord 𝑥) |
| 201 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ On → Ord ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) |
| 202 | | ordequn 6487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Ord
𝑥 ∧ Ord ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝐴 = (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 203 | 200, 201,
202 | syl2an 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ On) → (𝐴 = (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 204 | 199, 203 | biimtrid 242 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ∈ On) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 205 | 118, 198,
204 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴 → (𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))))) |
| 206 | 113, 194,
205 | mtord 880 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ¬ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴) |
| 207 | | onelss 6426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) |
| 208 | 183, 114,
207 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → 𝑥 ⊆ 𝐴) |
| 209 | | onelss 6426 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ On →
((card‘(𝑅1‘𝑦)) ∈ 𝐴 →
(card‘(𝑅1‘𝑦)) ⊆ 𝐴)) |
| 210 | 130, 142,
209 | sylsyld 61 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) →
(card‘(𝑅1‘𝑦)) ⊆ 𝐴)) |
| 211 | 210 | ralimdva 3167 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ 𝐴 ∈ Inacc) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → ∀𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ⊆ 𝐴)) |
| 212 | 211 | impr 454 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∀𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ⊆ 𝐴) |
| 213 | | iunss 5045 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ⊆ 𝐴) |
| 214 | 212, 213 | sylibr 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) ⊆ 𝐴) |
| 215 | 208, 214 | unssd 4192 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ⊆ 𝐴) |
| 216 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → 𝑥 = if(𝑥 ∈ On, 𝑥, ∅)) |
| 217 | | iuneq1 5008 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦)) = ∪
𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦))) |
| 218 | 216, 217 | uneq12d 4169 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦)))) |
| 219 | 218 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = if(𝑥 ∈ On, 𝑥, ∅) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ On ↔ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦))) ∈ On)) |
| 220 | | 0elon 6438 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∅
∈ On |
| 221 | 220 | elimel 4595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ On |
| 222 | 221 | elexi 3503 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ if(𝑥 ∈ On, 𝑥, ∅) ∈ V |
| 223 | | iunon 8379 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((if(𝑥 ∈ On,
𝑥, ∅) ∈ V ∧
∀𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦)) ∈ On) → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦)) ∈ On) |
| 224 | 222, 223 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑦 ∈ if
(𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦)) ∈ On → ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦)) ∈ On) |
| 225 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ if(𝑥 ∈ On, 𝑥, ∅) →
(card‘(𝑅1‘𝑦)) ∈ On) |
| 226 | 224, 225 | mprg 3067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦)) ∈ On |
| 227 | 221, 226 | onun2i 6506 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (if(𝑥 ∈ On, 𝑥, ∅) ∪ ∪ 𝑦 ∈ if (𝑥 ∈ On, 𝑥,
∅)(card‘(𝑅1‘𝑦))) ∈ On |
| 228 | 219, 227 | dedth 4584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ On) |
| 229 | 117, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
𝑥 → (𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ On) |
| 230 | 229 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝐴 ∧ Lim 𝑥) → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ On) |
| 231 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ Inacc ∧
∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴)) → 𝐴 ∈ On) |
| 232 | | onsseleq 6425 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∪ ∪ 𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ On ∧ 𝐴 ∈ On) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴))) |
| 233 | 230, 231,
232 | syl2an 596 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ⊆ 𝐴 ↔ ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴))) |
| 234 | 215, 233 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴 ∨ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴)) |
| 235 | 234 | orcomd 872 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴 ∨ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴)) |
| 236 | 235 | ord 865 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (¬ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) = 𝐴 → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴)) |
| 237 | 206, 236 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴) |
| 238 | 137 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (card‘𝐴) = 𝐴) |
| 239 | | iscard 10015 |
. . . . . . . . . . . . . . . 16
⊢
((card‘𝐴) =
𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴)) |
| 240 | 239 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢
((card‘𝐴) =
𝐴 → ∀𝑧 ∈ 𝐴 𝑧 ≺ 𝐴) |
| 241 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) → (𝑧 ≺ 𝐴 ↔ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≺ 𝐴)) |
| 242 | 241 | rspccv 3619 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝐴 𝑧 ≺ 𝐴 → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴 → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≺ 𝐴)) |
| 243 | 238, 240,
242 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → ((𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∈ 𝐴 → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≺ 𝐴)) |
| 244 | 237, 243 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) → (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≺ 𝐴) |
| 245 | | domsdomtr 9152 |
. . . . . . . . . . . . 13
⊢
(((𝑅1‘𝑥) ≼ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ∧ (𝑥 ∪ ∪
𝑦 ∈ 𝑥
(card‘(𝑅1‘𝑦))) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴) |
| 246 | 107, 244,
245 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ∧ Lim 𝑥) ∧ (𝐴 ∈ Inacc ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴))) →
(𝑅1‘𝑥) ≺ 𝐴) |
| 247 | 246 | exp43 436 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (Lim 𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)))) |
| 248 | 247 | com4l 92 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → (𝐴 ∈ Inacc → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝑅1‘𝑦) ≺ 𝐴) → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴)))) |
| 249 | 13, 17, 21, 28, 61, 248 | tfinds2 7885 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → (𝐴 ∈ Inacc → (𝑥 ∈ 𝐴 → (𝑅1‘𝑥) ≺ 𝐴))) |
| 250 | 249 | impd 410 |
. . . . . . . 8
⊢ (𝑥 ∈ On → ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴)) |
| 251 | 9, 250 | mpcom 38 |
. . . . . . 7
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≺ 𝐴) |
| 252 | | sdomdom 9020 |
. . . . . . 7
⊢
((𝑅1‘𝑥) ≺ 𝐴 → (𝑅1‘𝑥) ≼ 𝐴) |
| 253 | 251, 252 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝑥) ≼ 𝐴) |
| 254 | 253 | ralrimiva 3146 |
. . . . 5
⊢ (𝐴 ∈ Inacc →
∀𝑥 ∈ 𝐴
(𝑅1‘𝑥) ≼ 𝐴) |
| 255 | | iundom 10582 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ 𝐴) → ∪
𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴)) |
| 256 | 3, 254, 255 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥) ≼ (𝐴 × 𝐴)) |
| 257 | 7, 256 | eqbrtrd 5165 |
. . 3
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) ≼ (𝐴 × 𝐴)) |
| 258 | | winainf 10734 |
. . . . 5
⊢ (𝐴 ∈ Inaccw →
ω ⊆ 𝐴) |
| 259 | 1, 258 | syl 17 |
. . . 4
⊢ (𝐴 ∈ Inacc → ω
⊆ 𝐴) |
| 260 | | infxpen 10054 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |
| 261 | 3, 259, 260 | syl2anc 584 |
. . 3
⊢ (𝐴 ∈ Inacc → (𝐴 × 𝐴) ≈ 𝐴) |
| 262 | | domentr 9053 |
. . 3
⊢
(((𝑅1‘𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (𝑅1‘𝐴) ≼ 𝐴) |
| 263 | 257, 261,
262 | syl2anc 584 |
. 2
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) ≼ 𝐴) |
| 264 | | fvex 6919 |
. . 3
⊢
(𝑅1‘𝐴) ∈ V |
| 265 | 122 | fdmi 6747 |
. . . . 5
⊢ dom
𝑅1 = On |
| 266 | 2, 265 | eleqtrrdi 2852 |
. . . 4
⊢ (𝐴 ∈ Inaccw →
𝐴 ∈ dom
𝑅1) |
| 267 | | onssr1 9871 |
. . . 4
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴)) |
| 268 | 1, 266, 267 | 3syl 18 |
. . 3
⊢ (𝐴 ∈ Inacc → 𝐴 ⊆
(𝑅1‘𝐴)) |
| 269 | | ssdomg 9040 |
. . 3
⊢
((𝑅1‘𝐴) ∈ V → (𝐴 ⊆ (𝑅1‘𝐴) → 𝐴 ≼ (𝑅1‘𝐴))) |
| 270 | 264, 268,
269 | mpsyl 68 |
. 2
⊢ (𝐴 ∈ Inacc → 𝐴 ≼
(𝑅1‘𝐴)) |
| 271 | | sbth 9133 |
. 2
⊢
(((𝑅1‘𝐴) ≼ 𝐴 ∧ 𝐴 ≼ (𝑅1‘𝐴)) →
(𝑅1‘𝐴) ≈ 𝐴) |
| 272 | 263, 270,
271 | syl2anc 584 |
1
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) ≈ 𝐴) |