Step | Hyp | Ref
| Expression |
1 | | rankwflemb 8539 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑦)) |
2 | | suceloni 6905 |
. . . . 5
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
4 | 3 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
5 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢)) |
6 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢)) |
7 | 6 | imaeq2d 5385 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝑢))) |
8 | 5, 7 | sseq12d 3597 |
. . . . . . . 8
⊢ (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)))) |
9 | 8 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
10 | 4, 9 | syl6bb 275 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
11 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
12 | 11 | raleqdv 3121 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
13 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) |
14 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1‘𝑥)) |
15 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
16 | | rankr1ai 8544 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥) |
17 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (rank‘𝑧) →
(𝑅1‘𝑦) =
(𝑅1‘(rank‘𝑧))) |
18 | 17 | raleqdv 3121 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (rank‘𝑧) → (∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
19 | 18 | rspcv 3278 |
. . . . . . . . . . . . . . . 16
⊢
((rank‘𝑧)
∈ 𝑥 →
(∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
21 | | r1elwf 8542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → 𝑧 ∈ ∪
(𝑅1 “ On)) |
22 | | r1rankidb 8550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆
(𝑅1‘(rank‘𝑧))) |
23 | | ssralv 3629 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ⊆
(𝑅1‘(rank‘𝑧)) → (∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
25 | 20, 24 | syld 46 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
26 | 14, 15, 25 | sylc 63 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
27 | | rankval3b 8572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑧) = ∩ {𝑥
∈ On ∣ ∀𝑢
∈ 𝑧 (rank‘𝑢) ∈ 𝑥}) |
28 | 27 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) |
29 | 28 | biimpd 218 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) |
30 | | rankon 8541 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(rank‘𝑧)
∈ On |
31 | 30 | oneli 5752 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On) |
32 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤)) |
33 | 32 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) |
34 | 33 | onnminsb 6896 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ On → (𝑤 ∈ ∩ {𝑥
∈ On ∣ ∀𝑢
∈ 𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) |
35 | 31, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (rank‘𝑧) → (𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) |
36 | 29, 35 | sylcom 30 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) |
37 | 21, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) |
38 | 37 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤) |
39 | | rexnal 2978 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈
𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤) |
40 | 38, 39 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) |
42 | | r19.29 3054 |
. . . . . . . . . . . . 13
⊢
((∀𝑢 ∈
𝑧 (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)) ∧
∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) |
43 | 26, 41, 42 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) |
44 | | simp2 1055 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢 ∈ 𝑧) |
45 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
46 | | tcid 8498 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧)) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ⊆ (TC‘𝑧) |
48 | 47 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧)) |
49 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑢 → (rank‘𝑥) = (rank‘𝑢)) |
50 | 49 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤)) |
51 | 50 | rspcev 3282 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) |
52 | 51 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
53 | 44, 48, 52 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
54 | | simp3l 1082 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
55 | 54 | sseld 3567 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢)))) |
56 | | simp1l 1078 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥)) |
57 | | rankf 8540 |
. . . . . . . . . . . . . . . . . . 19
⊢
rank:∪ (𝑅1 “
On)⟶On |
58 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢
(rank:∪ (𝑅1 “
On)⟶On → rank Fn ∪
(𝑅1 “ On)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ rank Fn
∪ (𝑅1 “
On) |
60 | | r1tr 8522 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Tr
(𝑅1‘𝑥) |
61 | | trel 4687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Tr
(𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)) |
63 | | r1elwf 8542 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈
(𝑅1‘𝑥) → 𝑢 ∈ ∪
(𝑅1 “ On)) |
64 | | tcwf 8629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ∈ ∪ (𝑅1 “ On)) |
65 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(TC‘𝑢) ∈
V |
66 | 65 | r1elss 8552 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TC‘𝑢) ∈
∪ (𝑅1 “ On) ↔
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
67 | 64, 66 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
68 | 62, 63, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
69 | | fvelimab 6163 |
. . . . . . . . . . . . . . . . . 18
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑢)) ↔
∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤)) |
70 | 59, 68, 69 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤)) |
71 | 45 | tcel 8504 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧)) |
72 | | ssrexv 3630 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TC‘𝑢)
⊆ (TC‘𝑧) →
(∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
74 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
75 | 70, 74 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
76 | 44, 56, 75 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
77 | 55, 76 | syld 46 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
78 | | rankon 8541 |
. . . . . . . . . . . . . . . . . . 19
⊢
(rank‘𝑢)
∈ On |
79 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((rank‘𝑢)
∈ On → Ord (rank‘𝑢)) |
80 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ On → Ord 𝑤) |
81 | | ordtri3or 5672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Ord
(rank‘𝑢) ∧ Ord
𝑤) →
((rank‘𝑢) ∈
𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
82 | 79, 80, 81 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((rank‘𝑢)
∈ On ∧ 𝑤 ∈
On) → ((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
83 | 78, 31, 82 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
84 | | 3orass 1034 |
. . . . . . . . . . . . . . . . . 18
⊢
(((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) |
85 | 83, 84 | sylib 207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) |
86 | 85 | orcanai 950 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
87 | 86 | ad2ant2l 778 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
88 | 87 | 3adant2 1073 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
89 | 53, 77, 88 | mpjaod 395 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) |
90 | 89 | rexlimdv3a 3015 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
91 | 13, 43, 90 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) |
92 | 91 | expr 641 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
93 | | tcwf 8629 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) |
94 | | r1elssi 8551 |
. . . . . . . . . . . . . 14
⊢
((TC‘𝑧) ∈
∪ (𝑅1 “ On) →
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) |
95 | | fvelimab 6163 |
. . . . . . . . . . . . . 14
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
96 | 94, 95 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
97 | 59, 93, 96 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
98 | 21, 97 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
99 | 98 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
100 | 92, 99 | sylibrd 248 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧)))) |
101 | 100 | ssrdv 3574 |
. . . . . . . 8
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “
(TC‘𝑧))) |
102 | 101 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈
(𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))) |
103 | 102 | ex 449 |
. . . . . 6
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈
(𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
104 | 10, 12, 103 | tfis3 6949 |
. . . . 5
⊢ (suc
𝑦 ∈ On →
∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))) |
105 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴)) |
106 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴)) |
107 | 106 | imaeq2d 5385 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝐴))) |
108 | 105, 107 | sseq12d 3597 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “
(TC‘𝐴)))) |
109 | 108 | rspccv 3279 |
. . . . 5
⊢
(∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc
𝑦) → (rank‘𝐴) ⊆ (rank “
(TC‘𝐴)))) |
110 | 2, 104, 109 | 3syl 18 |
. . . 4
⊢ (𝑦 ∈ On → (𝐴 ∈
(𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))) |
111 | 110 | rexlimiv 3009 |
. . 3
⊢
(∃𝑦 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))) |
112 | 1, 111 | sylbi 206 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) ⊆
(rank “ (TC‘𝐴))) |
113 | | tcvalg 8497 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) = ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)}) |
114 | | r1rankidb 8550 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
115 | | r1tr 8522 |
. . . . 5
⊢ Tr
(𝑅1‘(rank‘𝐴)) |
116 | | fvex 6113 |
. . . . . . 7
⊢
(𝑅1‘(rank‘𝐴)) ∈ V |
117 | | sseq2 3590 |
. . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆
(𝑅1‘(rank‘𝐴)))) |
118 | | treq 4686 |
. . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr
(𝑅1‘(rank‘𝐴)))) |
119 | 117, 118 | anbi12d 743 |
. . . . . . 7
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))))) |
120 | 116, 119 | elab 3319 |
. . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴)))) |
121 | | intss1 4427 |
. . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
122 | 120, 121 | sylbir 224 |
. . . . 5
⊢ ((𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))) → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
123 | 114, 115,
122 | sylancl 693 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
124 | 113, 123 | eqsstrd 3602 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) ⊆
(𝑅1‘(rank‘𝐴))) |
125 | | imass2 5420 |
. . . 4
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “
(𝑅1‘(rank‘𝐴)))) |
126 | | ffun 5961 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) |
127 | 57, 126 | ax-mp 5 |
. . . . . . 7
⊢ Fun
rank |
128 | | fvelima 6158 |
. . . . . . 7
⊢ ((Fun
rank ∧ 𝑥 ∈ (rank
“ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) |
129 | 127, 128 | mpan 702 |
. . . . . 6
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) |
130 | | rankr1ai 8544 |
. . . . . . . 8
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴)) |
131 | | eleq1 2676 |
. . . . . . . 8
⊢
((rank‘𝑦) =
𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴))) |
132 | 130, 131 | syl5ibcom 234 |
. . . . . . 7
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))) |
133 | 132 | rexlimiv 3009 |
. . . . . 6
⊢
(∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)) |
134 | 129, 133 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴)) |
135 | 134 | ssriv 3572 |
. . . 4
⊢ (rank
“ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴) |
136 | 125, 135 | syl6ss 3580 |
. . 3
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴)) |
137 | 124, 136 | syl 17 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “
(TC‘𝐴)) ⊆
(rank‘𝐴)) |
138 | 112, 137 | eqssd 3585 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) = (rank
“ (TC‘𝐴))) |