Step | Hyp | Ref
| Expression |
1 | | df-ne 2782 |
. . . . 5
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
2 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(𝑅1‘𝐴) ∈ Tarski) |
3 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On) |
4 | | onwf 8576 |
. . . . . . . . . . . . . . . 16
⊢ On
⊆ ∪ (𝑅1 “
On) |
5 | 4 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → 𝐴 ∈ ∪ (𝑅1 “ On)) |
6 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(rank‘𝐴) =
(rank‘𝐴) |
7 | | rankr1c 8567 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
((rank‘𝐴) =
(rank‘𝐴) ↔
(¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴)) ∧ 𝐴 ∈ (𝑅1‘suc
(rank‘𝐴))))) |
8 | 6, 7 | mpbii 222 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴)) ∧ 𝐴 ∈ (𝑅1‘suc
(rank‘𝐴)))) |
9 | 5, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → (¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴)) ∧ 𝐴 ∈ (𝑅1‘suc
(rank‘𝐴)))) |
10 | 9 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈
(𝑅1‘(rank‘𝐴))) |
11 | | r1fnon 8513 |
. . . . . . . . . . . . . . . . 17
⊢
𝑅1 Fn On |
12 | | fndm 5904 |
. . . . . . . . . . . . . . . . 17
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ dom
𝑅1 = On |
14 | 13 | eleq2i 2680 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom
𝑅1 ↔ 𝐴 ∈ On) |
15 | | rankonid 8575 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom
𝑅1 ↔ (rank‘𝐴) = 𝐴) |
16 | 14, 15 | bitr3i 265 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On ↔
(rank‘𝐴) = 𝐴) |
17 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢
((rank‘𝐴) =
𝐴 →
(𝑅1‘(rank‘𝐴)) = (𝑅1‘𝐴)) |
18 | 16, 17 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On →
(𝑅1‘(rank‘𝐴)) = (𝑅1‘𝐴)) |
19 | 10, 18 | neleqtrd 2709 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈
(𝑅1‘𝐴)) |
20 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → ¬ 𝐴 ∈ (𝑅1‘𝐴)) |
21 | | onssr1 8577 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴)) |
22 | 14, 21 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → 𝐴 ⊆
(𝑅1‘𝐴)) |
23 | | tsken 9455 |
. . . . . . . . . . . . 13
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ⊆ (𝑅1‘𝐴)) → (𝐴 ≈ (𝑅1‘𝐴) ∨ 𝐴 ∈ (𝑅1‘𝐴))) |
24 | 22, 23 | sylan2 490 |
. . . . . . . . . . . 12
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → (𝐴 ≈ (𝑅1‘𝐴) ∨ 𝐴 ∈ (𝑅1‘𝐴))) |
25 | 24 | ord 391 |
. . . . . . . . . . 11
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → (¬ 𝐴 ≈ (𝑅1‘𝐴) → 𝐴 ∈ (𝑅1‘𝐴))) |
26 | 20, 25 | mt3d 139 |
. . . . . . . . . 10
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) → 𝐴 ≈ (𝑅1‘𝐴)) |
27 | 2, 3, 26 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ (𝑅1‘𝐴)) |
28 | | carden2b 8676 |
. . . . . . . . 9
⊢ (𝐴 ≈
(𝑅1‘𝐴) → (card‘𝐴) =
(card‘(𝑅1‘𝐴))) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → (card‘𝐴) =
(card‘(𝑅1‘𝐴))) |
30 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → 𝐴 ∈ On) |
31 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝐴) ∈
Tarski) |
32 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → 𝐴 ⊆ (𝑅1‘𝐴)) |
33 | 32 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (𝑅1‘𝐴)) |
34 | | tsksdom 9457 |
. . . . . . . . . . . . 13
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝑥 ≺ (𝑅1‘𝐴)) |
35 | 31, 33, 34 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (𝑅1‘𝐴)) |
36 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ On) |
37 | 26 | ensymd 7893 |
. . . . . . . . . . . . 13
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧ 𝐴 ∈ On) →
(𝑅1‘𝐴) ≈ 𝐴) |
38 | 31, 36, 37 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → (𝑅1‘𝐴) ≈ 𝐴) |
39 | | sdomentr 7979 |
. . . . . . . . . . . 12
⊢ ((𝑥 ≺
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≈ 𝐴) → 𝑥 ≺ 𝐴) |
40 | 35, 38, 39 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ 𝐴) |
41 | 40 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴) |
42 | | iscard 8684 |
. . . . . . . . . 10
⊢
((card‘𝐴) =
𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴)) |
43 | 30, 41, 42 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (card‘𝐴) = 𝐴) |
44 | 43 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → (card‘𝐴) = 𝐴) |
45 | 29, 44 | eqtr3d 2646 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(card‘(𝑅1‘𝐴)) = 𝐴) |
46 | | r10 8514 |
. . . . . . . . . . 11
⊢
(𝑅1‘∅) = ∅ |
47 | | on0eln0 5697 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
48 | 47 | biimpar 501 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅
∈ 𝐴) |
49 | | r1sdom 8520 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) →
(𝑅1‘∅) ≺
(𝑅1‘𝐴)) |
50 | 48, 49 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) →
(𝑅1‘∅) ≺
(𝑅1‘𝐴)) |
51 | 46, 50 | syl5eqbrr 4619 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) → ∅
≺ (𝑅1‘𝐴)) |
52 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(𝑅1‘𝐴) ∈ V |
53 | 52 | 0sdom 7976 |
. . . . . . . . . 10
⊢ (∅
≺ (𝑅1‘𝐴) ↔ (𝑅1‘𝐴) ≠ ∅) |
54 | 51, 53 | sylib 207 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅) →
(𝑅1‘𝐴) ≠ ∅) |
55 | 54 | adantlr 747 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(𝑅1‘𝐴) ≠ ∅) |
56 | | tskcard 9482 |
. . . . . . . 8
⊢
(((𝑅1‘𝐴) ∈ Tarski ∧
(𝑅1‘𝐴) ≠ ∅) →
(card‘(𝑅1‘𝐴)) ∈ Inacc) |
57 | 2, 55, 56 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) →
(card‘(𝑅1‘𝐴)) ∈ Inacc) |
58 | 45, 57 | eqeltrrd 2689 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ Inacc) |
59 | 58 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (𝐴 ≠ ∅ → 𝐴 ∈ Inacc)) |
60 | 1, 59 | syl5bir 232 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (¬ 𝐴 = ∅ → 𝐴 ∈ Inacc)) |
61 | 60 | orrd 392 |
. . 3
⊢ ((𝐴 ∈ On ∧
(𝑅1‘𝐴) ∈ Tarski) → (𝐴 = ∅ ∨ 𝐴 ∈ Inacc)) |
62 | 61 | ex 449 |
. 2
⊢ (𝐴 ∈ On →
((𝑅1‘𝐴) ∈ Tarski → (𝐴 = ∅ ∨ 𝐴 ∈ Inacc))) |
63 | | fveq2 6103 |
. . . . 5
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) =
(𝑅1‘∅)) |
64 | 63, 46 | syl6eq 2660 |
. . . 4
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) = ∅) |
65 | | 0tsk 9456 |
. . . 4
⊢ ∅
∈ Tarski |
66 | 64, 65 | syl6eqel 2696 |
. . 3
⊢ (𝐴 = ∅ →
(𝑅1‘𝐴) ∈ Tarski) |
67 | | inatsk 9479 |
. . 3
⊢ (𝐴 ∈ Inacc →
(𝑅1‘𝐴) ∈ Tarski) |
68 | 66, 67 | jaoi 393 |
. 2
⊢ ((𝐴 = ∅ ∨ 𝐴 ∈ Inacc) →
(𝑅1‘𝐴) ∈ Tarski) |
69 | 62, 68 | impbid1 214 |
1
⊢ (𝐴 ∈ On →
((𝑅1‘𝐴) ∈ Tarski ↔ (𝐴 = ∅ ∨ 𝐴 ∈ Inacc))) |