Step | Hyp | Ref
| Expression |
1 | | rankwflemb 9422 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑦)) |
2 | | suceloni 7601 |
. . . . 5
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
3 | | fveq2 6726 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
4 | 3 | raleqdv 3332 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
5 | | fveq2 6726 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢)) |
6 | | fveq2 6726 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢)) |
7 | 6 | imaeq2d 5938 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝑢))) |
8 | 5, 7 | sseq12d 3943 |
. . . . . . . 8
⊢ (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)))) |
9 | 8 | cbvralvw 3365 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
10 | 4, 9 | bitrdi 290 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
11 | | fveq2 6726 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
12 | 11 | raleqdv 3332 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
13 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) |
14 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1‘𝑥)) |
15 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
16 | | rankr1ai 9427 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥) |
17 | | fveq2 6726 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (rank‘𝑧) →
(𝑅1‘𝑦) =
(𝑅1‘(rank‘𝑧))) |
18 | 17 | raleqdv 3332 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (rank‘𝑧) → (∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) |
19 | 18 | rspcv 3539 |
. . . . . . . . . . . . . . . 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 9425 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → 𝑧 ∈ ∪
(𝑅1 “ On)) |
22 | | r1rankidb 9433 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆
(𝑅1‘(rank‘𝑧))) |
23 | | ssralv 3976 |
. . . . . . . . . . . . . . . 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 9455 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑧) = ∩ {𝑥
∈ On ∣ ∀𝑢
∈ 𝑧 (rank‘𝑢) ∈ 𝑥}) |
28 | 27 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) |
29 | 28 | biimpd 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) |
30 | | rankon 9424 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(rank‘𝑧)
∈ On |
31 | 30 | oneli 6330 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On) |
32 | | eleq2w 2822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤)) |
33 | 32 | ralbidv 3119 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) |
34 | 33 | onnminsb 7592 |
. . . . . . . . . . . . . . . . . . 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 410 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤) |
39 | | rexnal 3164 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈
𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤) |
40 | 38, 39 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) |
41 | 40 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) |
42 | | r19.29 3182 |
. . . . . . . . . . . . 13
⊢
((∀𝑢 ∈
𝑧 (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)) ∧
∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) |
43 | 26, 41, 42 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) |
44 | | simp2 1139 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢 ∈ 𝑧) |
45 | | tcid 9368 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧)) |
46 | 45 | elv 3421 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ⊆ (TC‘𝑧) |
47 | 46 | sseli 3905 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧)) |
48 | | fveqeq2 6735 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤)) |
49 | 48 | rspcev 3544 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) |
50 | 49 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
51 | 44, 47, 50 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
52 | | simp3l 1203 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) |
53 | 52 | sseld 3909 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢)))) |
54 | | simp1l 1199 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥)) |
55 | | rankf 9423 |
. . . . . . . . . . . . . . . . . . 19
⊢
rank:∪ (𝑅1 “
On)⟶On |
56 | | ffn 6554 |
. . . . . . . . . . . . . . . . . . 19
⊢
(rank:∪ (𝑅1 “
On)⟶On → rank Fn ∪
(𝑅1 “ On)) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ rank Fn
∪ (𝑅1 “
On) |
58 | | r1tr 9405 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Tr
(𝑅1‘𝑥) |
59 | | trel 5177 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Tr
(𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)) |
61 | | r1elwf 9425 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈
(𝑅1‘𝑥) → 𝑢 ∈ ∪
(𝑅1 “ On)) |
62 | | tcwf 9512 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ∈ ∪ (𝑅1 “ On)) |
63 | | fvex 6739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(TC‘𝑢) ∈
V |
64 | 63 | r1elss 9435 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TC‘𝑢) ∈
∪ (𝑅1 “ On) ↔
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
65 | 62, 64 | sylib 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
66 | 60, 61, 65 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) |
67 | | fvelimab 6793 |
. . . . . . . . . . . . . . . . . 18
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑢)) ↔
∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤)) |
68 | 57, 66, 67 | sylancr 590 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤)) |
69 | | vex 3419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑧 ∈ V |
70 | 69 | tcel 9374 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧)) |
71 | | ssrexv 3977 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TC‘𝑢)
⊆ (TC‘𝑧) →
(∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
73 | 72 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
74 | 68, 73 | sylbid 243 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
75 | 44, 54, 74 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
76 | 53, 75 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
77 | | rankon 9424 |
. . . . . . . . . . . . . . . . . . 19
⊢
(rank‘𝑢)
∈ On |
78 | | eloni 6232 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((rank‘𝑢)
∈ On → Ord (rank‘𝑢)) |
79 | | eloni 6232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ On → Ord 𝑤) |
80 | | ordtri3or 6254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Ord
(rank‘𝑢) ∧ Ord
𝑤) →
((rank‘𝑢) ∈
𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
81 | 78, 79, 80 | syl2an 599 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((rank‘𝑢)
∈ On ∧ 𝑤 ∈
On) → ((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
82 | 77, 31, 81 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
83 | | 3orass 1092 |
. . . . . . . . . . . . . . . . . 18
⊢
(((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) |
84 | 82, 83 | sylib 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) |
85 | 84 | orcanai 1003 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
86 | 85 | ad2ant2l 746 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
87 | 86 | 3adant2 1133 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) |
88 | 51, 76, 87 | mpjaod 860 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) |
89 | 88 | rexlimdv3a 3212 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
90 | 13, 43, 89 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) |
91 | 90 | expr 460 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
92 | | tcwf 9512 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) |
93 | | r1elssi 9434 |
. . . . . . . . . . . . . 14
⊢
((TC‘𝑧) ∈
∪ (𝑅1 “ On) →
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) |
94 | | fvelimab 6793 |
. . . . . . . . . . . . . 14
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
95 | 93, 94 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
96 | 57, 92, 95 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) |
97 | 21, 96 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
98 | 97 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) |
99 | 91, 98 | sylibrd 262 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧)))) |
100 | 99 | ssrdv 3916 |
. . . . . . . 8
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “
(TC‘𝑧))) |
101 | 100 | ralrimiva 3106 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈
(𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))) |
102 | 101 | ex 416 |
. . . . . 6
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈
(𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) |
103 | 10, 12, 102 | tfis3 7645 |
. . . . 5
⊢ (suc
𝑦 ∈ On →
∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))) |
104 | | fveq2 6726 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴)) |
105 | | fveq2 6726 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴)) |
106 | 105 | imaeq2d 5938 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝐴))) |
107 | 104, 106 | sseq12d 3943 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “
(TC‘𝐴)))) |
108 | 107 | rspccv 3541 |
. . . . 5
⊢
(∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc
𝑦) → (rank‘𝐴) ⊆ (rank “
(TC‘𝐴)))) |
109 | 2, 103, 108 | 3syl 18 |
. . . 4
⊢ (𝑦 ∈ On → (𝐴 ∈
(𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))) |
110 | 109 | rexlimiv 3206 |
. . 3
⊢
(∃𝑦 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))) |
111 | 1, 110 | sylbi 220 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) ⊆
(rank “ (TC‘𝐴))) |
112 | | tcvalg 9367 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) = ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)}) |
113 | | r1rankidb 9433 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) |
114 | | r1tr 9405 |
. . . . 5
⊢ Tr
(𝑅1‘(rank‘𝐴)) |
115 | | fvex 6739 |
. . . . . . 7
⊢
(𝑅1‘(rank‘𝐴)) ∈ V |
116 | | sseq2 3936 |
. . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆
(𝑅1‘(rank‘𝐴)))) |
117 | | treq 5176 |
. . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr
(𝑅1‘(rank‘𝐴)))) |
118 | 116, 117 | anbi12d 634 |
. . . . . . 7
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))))) |
119 | 115, 118 | elab 3594 |
. . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴)))) |
120 | | intss1 4883 |
. . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
121 | 119, 120 | sylbir 238 |
. . . . 5
⊢ ((𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))) → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
122 | 113, 114,
121 | sylancl 589 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) |
123 | 112, 122 | eqsstrd 3948 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) ⊆
(𝑅1‘(rank‘𝐴))) |
124 | | imass2 5979 |
. . . 4
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “
(𝑅1‘(rank‘𝐴)))) |
125 | | ffun 6557 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) |
126 | 55, 125 | ax-mp 5 |
. . . . . . 7
⊢ Fun
rank |
127 | | fvelima 6787 |
. . . . . . 7
⊢ ((Fun
rank ∧ 𝑥 ∈ (rank
“ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) |
128 | 126, 127 | mpan 690 |
. . . . . 6
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) |
129 | | rankr1ai 9427 |
. . . . . . . 8
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴)) |
130 | | eleq1 2826 |
. . . . . . . 8
⊢
((rank‘𝑦) =
𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴))) |
131 | 129, 130 | syl5ibcom 248 |
. . . . . . 7
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))) |
132 | 131 | rexlimiv 3206 |
. . . . . 6
⊢
(∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)) |
133 | 128, 132 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴)) |
134 | 133 | ssriv 3914 |
. . . 4
⊢ (rank
“ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴) |
135 | 124, 134 | sstrdi 3922 |
. . 3
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴)) |
136 | 123, 135 | syl 17 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “
(TC‘𝐴)) ⊆
(rank‘𝐴)) |
137 | 111, 136 | eqssd 3927 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) = (rank
“ (TC‘𝐴))) |