| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . . . 5
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
| 2 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(𝑅1‘𝐴) ∈ Tarski) |
| 3 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On) |
| 4 | | onwf 9870 |
. . . . . . . . . . . . . . . 16
⊢ On
⊆ ∪ (𝑅1 “
On) |
| 5 | 4 | sseli 3979 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → 𝐴 ∈ ∪ (𝑅1 “ On)) |
| 6 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(rank‘𝐴) =
(rank‘𝐴) |
| 7 | | rankr1c 9861 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
((rank‘𝐴) =
(rank‘𝐴) ↔
(¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴)) ∧ 𝐴 ∈ (𝑅1‘suc
(rank‘𝐴))))) |
| 8 | 6, 7 | mpbii 233 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴)) ∧ 𝐴 ∈ (𝑅1‘suc
(rank‘𝐴)))) |
| 9 | 5, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → (¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴)) ∧ 𝐴 ∈ (𝑅1‘suc
(rank‘𝐴)))) |
| 10 | 9 | simpld 494 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴))) |
| 11 | | r1fnon 9807 |
. . . . . . . . . . . . . . . . 17
⊢
𝑅1 Fn On |
| 12 | 11 | fndmi 6672 |
. . . . . . . . . . . . . . . 16
⊢ dom
𝑅1 = On |
| 13 | 12 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom
𝑅1 ↔ 𝐴 ∈ On) |
| 14 | | rankonid 9869 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom
𝑅1 ↔ (rank‘𝐴) = 𝐴) |
| 15 | 13, 14 | bitr3i 277 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On ↔
(rank‘𝐴) = 𝐴) |
| 16 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢
((rank‘𝐴) =
𝐴 →
(𝑅1‘(rank‘𝐴)) = (𝑅1‘𝐴)) |
| 17 | 15, 16 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On →
(𝑅1‘(rank‘𝐴)) = (𝑅1‘𝐴)) |
| 18 | 10, 17 | neleqtrd 2863 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈
(𝑅1‘𝐴)) |
| 19 | 18 | adantl 481 |
. . . . . . . . . . 11
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → ¬ 𝐴 ∈ (𝑅1‘𝐴)) |
| 20 | | onssr1 9871 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴)) |
| 21 | 13, 20 | sylbir 235 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → 𝐴 ⊆
(𝑅1‘𝐴)) |
| 22 | | tsken 10794 |
. . . . . . . . . . . . 13
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ⊆ (𝑅1‘𝐴)) → (𝐴 ≈ (𝑅1‘𝐴) ∨ 𝐴 ∈ (𝑅1‘𝐴))) |
| 23 | 21, 22 | sylan2 593 |
. . . . . . . . . . . 12
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → (𝐴 ≈ (𝑅1‘𝐴) ∨ 𝐴 ∈ (𝑅1‘𝐴))) |
| 24 | 23 | ord 865 |
. . . . . . . . . . 11
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → (¬ 𝐴 ≈ (𝑅1‘𝐴) → 𝐴 ∈ (𝑅1‘𝐴))) |
| 25 | 19, 24 | mt3d 148 |
. . . . . . . . . 10
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → 𝐴 ≈ (𝑅1‘𝐴)) |
| 26 | 2, 3, 25 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ (𝑅1‘𝐴)) |
| 27 | | carden2b 10007 |
. . . . . . . . 9
⊢ (𝐴 ≈
(𝑅1‘𝐴) → (card‘𝐴) =
(card‘(𝑅1‘𝐴))) |
| 28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → (card‘𝐴) =
(card‘(𝑅1‘𝐴))) |
| 29 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → 𝐴 ∈ On) |
| 30 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝐴) ∈
Tarski) |
| 31 | 21 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → 𝐴 ⊆ (𝑅1‘𝐴)) |
| 32 | 31 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (𝑅1‘𝐴)) |
| 33 | | tsksdom 10796 |
. . . . . . . . . . . . 13
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝑥 ≺ (𝑅1‘𝐴)) |
| 34 | 30, 32, 33 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (𝑅1‘𝐴)) |
| 35 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ On) |
| 36 | 25 | ensymd 9045 |
. . . . . . . . . . . . 13
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) →
(𝑅1‘𝐴) ≈ 𝐴) |
| 37 | 30, 35, 36 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝐴) ≈ 𝐴) |
| 38 | | sdomentr 9151 |
. . . . . . . . . . . 12
⊢ ((𝑥 ≺
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≈ 𝐴) → 𝑥 ≺ 𝐴) |
| 39 | 34, 37, 38 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ 𝐴) |
| 40 | 39 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴) |
| 41 | | iscard 10015 |
. . . . . . . . . 10
⊢
((card‘𝐴) =
𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴)) |
| 42 | 29, 40, 41 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (card‘𝐴) = 𝐴) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → (card‘𝐴) = 𝐴) |
| 44 | 28, 43 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(card‘(𝑅1‘𝐴)) = 𝐴) |
| 45 | | r10 9808 |
. . . . . . . . . . 11
⊢
(𝑅1‘∅) = ∅ |
| 46 | | on0eln0 6440 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 47 | 46 | biimpar 477 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅
∈ 𝐴) |
| 48 | | r1sdom 9814 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) →
(𝑅1‘∅) ≺
(𝑅1‘𝐴)) |
| 49 | 47, 48 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) →
(𝑅1‘∅) ≺
(𝑅1‘𝐴)) |
| 50 | 45, 49 | eqbrtrrid 5179 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅
≺ (𝑅1‘𝐴)) |
| 51 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(𝑅1‘𝐴) ∈ V |
| 52 | 51 | 0sdom 9147 |
. . . . . . . . . 10
⊢ (∅
≺ (𝑅1‘𝐴) ↔ (𝑅1‘𝐴) ≠ ∅) |
| 53 | 50, 52 | sylib 218 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) →
(𝑅1‘𝐴) ≠ ∅) |
| 54 | 53 | adantlr 715 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(𝑅1‘𝐴) ≠ ∅) |
| 55 | | tskcard 10821 |
. . . . . . . 8
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧
(𝑅1‘𝐴) ≠ ∅) →
(card‘(𝑅1‘𝐴)) ∈ Inacc) |
| 56 | 2, 54, 55 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(card‘(𝑅1‘𝐴)) ∈ Inacc) |
| 57 | 44, 56 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ Inacc) |
| 58 | 57 | ex 412 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (𝐴 ≠ ∅ → 𝐴 ∈ Inacc)) |
| 59 | 1, 58 | biimtrrid 243 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (¬ 𝐴 = ∅ → 𝐴 ∈ Inacc)) |
| 60 | 59 | orrd 864 |
. . 3
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (𝐴 = ∅ ∨ 𝐴 ∈ Inacc)) |
| 61 | 60 | ex 412 |
. 2
⊢ (𝐴 ∈ On →
((𝑅1‘𝐴) ∈ Tarski → (𝐴 = ∅ ∨ 𝐴 ∈ Inacc))) |
| 62 | | fveq2 6906 |
. . . . 5
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) =
(𝑅1‘∅)) |
| 63 | 62, 45 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) = ∅) |
| 64 | | 0tsk 10795 |
. . . 4
⊢ ∅
∈ Tarski |
| 65 | 63, 64 | eqeltrdi 2849 |
. . 3
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) ∈ Tarski) |
| 66 | | inatsk 10818 |
. . 3
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) ∈ Tarski) |
| 67 | 65, 66 | jaoi 858 |
. 2
⊢ ((𝐴 = ∅ ∨ 𝐴 ∈ Inacc) →
(𝑅1‘𝐴) ∈ Tarski) |
| 68 | 61, 67 | impbid1 225 |
1
⊢ (𝐴 ∈ On →
((𝑅1‘𝐴) ∈ Tarski ↔ (𝐴 = ∅ ∨ 𝐴 ∈ Inacc))) |