Step | Hyp | Ref
| Expression |
1 | | rankwflemb 8831 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑦)) |
2 | | suceloni 7179 |
. . . . 5
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
3 | | fveq2 6353 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
4 | 3 | raleqdv 3283 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
5 | | fveq2 6353 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢)) |
6 | | fveq2 6353 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢)) |
7 | 6 | imaeq2d 5624 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝑢))) |
8 | 5, 7 | sseq12d 3775 |
. . . . . . . 8
⊢ (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)))) |
9 | 8 | cbvralv 3310 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
10 | 4, 9 | syl6bb 276 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
11 | | fveq2 6353 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
12 | 11 | raleqdv 3283 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
13 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) |
14 | | simprl 811 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1‘𝑥)) |
15 | | simplr 809 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
16 | | rankr1ai 8836 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥) |
17 | | fveq2 6353 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (rank‘𝑧) →
(𝑅1‘𝑦) =
(𝑅1‘(rank‘𝑧))) |
18 | 17 | raleqdv 3283 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (rank‘𝑧) → (∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
19 | 18 | rspcv 3445 |
. . . . . . . . . . . . . . . 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 8834 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → 𝑧 ∈ ∪
(𝑅1 “ On)) |
22 | | r1rankidb 8842 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆
(𝑅1‘(rank‘𝑧))) |
23 | | ssralv 3807 |
. . . . . . . . . . . . . . . 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 47 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
26 | 14, 15, 25 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
27 | | rankval3b 8864 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑧) = ∩ {𝑥
∈ On ∣ ∀𝑢
∈ 𝑧 (rank‘𝑢) ∈ 𝑥}) |
28 | 27 | eleq2d 2825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) |
29 | 28 | biimpd 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) |
30 | | rankon 8833 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(rank‘𝑧)
∈ On |
31 | 30 | oneli 5996 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On) |
32 | | eleq2w 2823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤)) |
33 | 32 | ralbidv 3124 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) |
34 | 33 | onnminsb 7170 |
. . . . . . . . . . . . . . . . . . 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 3133 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈
𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤) |
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) |
41 | 40 | adantl 473 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) |
42 | | r19.29 3210 |
. . . . . . . . . . . . 13
⊢
((∀𝑢 ∈
𝑧 (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)) ∧
∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) |
43 | 26, 41, 42 | syl2anc 696 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) |
44 | | simp2 1132 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢 ∈ 𝑧) |
45 | | vex 3343 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
46 | | tcid 8790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧)) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ⊆ (TC‘𝑧) |
48 | 47 | sseli 3740 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧)) |
49 | | fveq2 6353 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑢 → (rank‘𝑥) = (rank‘𝑢)) |
50 | 49 | eqeq1d 2762 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤)) |
51 | 50 | rspcev 3449 |
. . . . . . . . . . . . . . . 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 1244 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
55 | 54 | sseld 3743 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢)))) |
56 | | simp1l 1240 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥)) |
57 | | rankf 8832 |
. . . . . . . . . . . . . . . . . . 19
⊢
rank:∪ (𝑅1 “
On)⟶On |
58 | | ffn 6206 |
. . . . . . . . . . . . . . . . . . 19
⊢
(rank:∪ (𝑅1 “
On)⟶On → rank Fn ∪
(𝑅1 “ On)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ rank Fn
∪ (𝑅1 “
On) |
60 | | r1tr 8814 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Tr
(𝑅1‘𝑥) |
61 | | trel 4911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Tr
(𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)) |
63 | | r1elwf 8834 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈
(𝑅1‘𝑥) → 𝑢 ∈ ∪
(𝑅1 “ On)) |
64 | | tcwf 8921 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ∈ ∪ (𝑅1 “ On)) |
65 | | fvex 6363 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(TC‘𝑢) ∈
V |
66 | 65 | r1elss 8844 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TC‘𝑢) ∈
∪ (𝑅1 “ On) ↔
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
67 | 64, 66 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
68 | 62, 63, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
69 | | fvelimab 6416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑢)) ↔
∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤)) |
70 | 59, 68, 69 | sylancr 698 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤)) |
71 | 45 | tcel 8796 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧)) |
72 | | ssrexv 3808 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TC‘𝑢)
⊆ (TC‘𝑧) →
(∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
74 | 73 | adantr 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
75 | 70, 74 | sylbid 230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
76 | 44, 56, 75 | syl2anc 696 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
77 | 55, 76 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
78 | | rankon 8833 |
. . . . . . . . . . . . . . . . . . 19
⊢
(rank‘𝑢)
∈ On |
79 | | eloni 5894 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((rank‘𝑢)
∈ On → Ord (rank‘𝑢)) |
80 | | eloni 5894 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ On → Ord 𝑤) |
81 | | ordtri3or 5916 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Ord
(rank‘𝑢) ∧ Ord
𝑤) →
((rank‘𝑢) ∈
𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
82 | 79, 80, 81 | syl2an 495 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((rank‘𝑢)
∈ On ∧ 𝑤 ∈
On) → ((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
83 | 78, 31, 82 | sylancr 698 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
84 | | 3orass 1075 |
. . . . . . . . . . . . . . . . . 18
⊢
(((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) |
85 | 83, 84 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) |
86 | 85 | orcanai 990 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
87 | 86 | ad2ant2l 799 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
88 | 87 | 3adant2 1126 |
. . . . . . . . . . . . . 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 3171 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
91 | 13, 43, 90 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) |
92 | 91 | expr 644 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
93 | | tcwf 8921 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) |
94 | | r1elssi 8843 |
. . . . . . . . . . . . . 14
⊢
((TC‘𝑧) ∈
∪ (𝑅1 “ On) →
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) |
95 | | fvelimab 6416 |
. . . . . . . . . . . . . 14
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
96 | 94, 95 | sylan2 492 |
. . . . . . . . . . . . 13
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
97 | 59, 93, 96 | sylancr 698 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
98 | 21, 97 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
99 | 98 | adantl 473 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
100 | 92, 99 | sylibrd 249 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧)))) |
101 | 100 | ssrdv 3750 |
. . . . . . . 8
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “
(TC‘𝑧))) |
102 | 101 | ralrimiva 3104 |
. . . . . . 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 7223 |
. . . . 5
⊢ (suc
𝑦 ∈ On →
∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))) |
105 | | fveq2 6353 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴)) |
106 | | fveq2 6353 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴)) |
107 | 106 | imaeq2d 5624 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝐴))) |
108 | 105, 107 | sseq12d 3775 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “
(TC‘𝐴)))) |
109 | 108 | rspccv 3446 |
. . . . 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 3165 |
. . 3
⊢
(∃𝑦 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))) |
112 | 1, 111 | sylbi 207 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) ⊆
(rank “ (TC‘𝐴))) |
113 | | tcvalg 8789 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) = ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)}) |
114 | | r1rankidb 8842 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
115 | | r1tr 8814 |
. . . . 5
⊢ Tr
(𝑅1‘(rank‘𝐴)) |
116 | | fvex 6363 |
. . . . . . 7
⊢
(𝑅1‘(rank‘𝐴)) ∈ V |
117 | | sseq2 3768 |
. . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆
(𝑅1‘(rank‘𝐴)))) |
118 | | treq 4910 |
. . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr
(𝑅1‘(rank‘𝐴)))) |
119 | 117, 118 | anbi12d 749 |
. . . . . . 7
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))))) |
120 | 116, 119 | elab 3490 |
. . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴)))) |
121 | | intss1 4644 |
. . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
122 | 120, 121 | sylbir 225 |
. . . . 5
⊢ ((𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))) → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
123 | 114, 115,
122 | sylancl 697 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
124 | 113, 123 | eqsstrd 3780 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) ⊆
(𝑅1‘(rank‘𝐴))) |
125 | | imass2 5659 |
. . . 4
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “
(𝑅1‘(rank‘𝐴)))) |
126 | | ffun 6209 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) |
127 | 57, 126 | ax-mp 5 |
. . . . . . 7
⊢ Fun
rank |
128 | | fvelima 6411 |
. . . . . . 7
⊢ ((Fun
rank ∧ 𝑥 ∈ (rank
“ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) |
129 | 127, 128 | mpan 708 |
. . . . . 6
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) |
130 | | rankr1ai 8836 |
. . . . . . . 8
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴)) |
131 | | eleq1 2827 |
. . . . . . . 8
⊢
((rank‘𝑦) =
𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴))) |
132 | 130, 131 | syl5ibcom 235 |
. . . . . . 7
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))) |
133 | 132 | rexlimiv 3165 |
. . . . . 6
⊢
(∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)) |
134 | 129, 133 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴)) |
135 | 134 | ssriv 3748 |
. . . 4
⊢ (rank
“ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴) |
136 | 125, 135 | syl6ss 3756 |
. . 3
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴)) |
137 | 124, 136 | syl 17 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “
(TC‘𝐴)) ⊆
(rank‘𝐴)) |
138 | 112, 137 | eqssd 3761 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) = (rank
“ (TC‘𝐴))) |