| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rankwflemb 9834 | . . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc
𝑦)) | 
| 2 |  | onsuc 7832 | . . . . 5
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) | 
| 3 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) | 
| 4 | 3 | raleqdv 3325 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) | 
| 5 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢)) | 
| 6 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢)) | 
| 7 | 6 | imaeq2d 6077 | . . . . . . . . 9
⊢ (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝑢))) | 
| 8 | 5, 7 | sseq12d 4016 | . . . . . . . 8
⊢ (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)))) | 
| 9 | 8 | cbvralvw 3236 | . . . . . . 7
⊢
(∀𝑧 ∈
(𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) | 
| 10 | 4, 9 | bitrdi 287 | . . . . . 6
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) | 
| 11 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) | 
| 12 | 11 | raleqdv 3325 | . . . . . 6
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) | 
| 13 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) | 
| 14 |  | simprl 770 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1‘𝑥)) | 
| 15 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) | 
| 16 |  | rankr1ai 9839 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥) | 
| 17 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (rank‘𝑧) →
(𝑅1‘𝑦) =
(𝑅1‘(rank‘𝑧))) | 
| 18 | 17 | raleqdv 3325 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (rank‘𝑧) → (∀𝑢 ∈
(𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈
(𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))) | 
| 19 | 18 | rspcv 3617 | . . . . . . . . . . . . . . . 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 9837 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(𝑅1‘𝑥) → 𝑧 ∈ ∪
(𝑅1 “ On)) | 
| 22 |  | r1rankidb 9845 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆
(𝑅1‘(rank‘𝑧))) | 
| 23 |  | ssralv 4051 | . . . . . . . . . . . . . . . 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 9867 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑧) = ∩ {𝑥
∈ On ∣ ∀𝑢
∈ 𝑧 (rank‘𝑢) ∈ 𝑥}) | 
| 28 | 27 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) | 
| 29 | 28 | biimpd 229 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})) | 
| 30 |  | rankon 9836 | . . . . . . . . . . . . . . . . . . . 20
⊢
(rank‘𝑧)
∈ On | 
| 31 | 30 | oneli 6497 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On) | 
| 32 |  | eleq2w 2824 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤)) | 
| 33 | 32 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)) | 
| 34 | 33 | onnminsb 7820 | . . . . . . . . . . . . . . . . . . 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 406 | . . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤) | 
| 39 |  | rexnal 3099 | . . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈
𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤) | 
| 40 | 38, 39 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) | 
| 42 |  | r19.29 3113 | . . . . . . . . . . . . 13
⊢
((∀𝑢 ∈
𝑧 (rank‘𝑢) ⊆ (rank “
(TC‘𝑢)) ∧
∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) | 
| 43 | 26, 41, 42 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) | 
| 44 |  | simp2 1137 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢 ∈ 𝑧) | 
| 45 |  | tcid 9780 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧)) | 
| 46 | 45 | elv 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑧 ⊆ (TC‘𝑧) | 
| 47 | 46 | sseli 3978 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧)) | 
| 48 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤)) | 
| 49 | 48 | rspcev 3621 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤) | 
| 50 | 49 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 51 | 44, 47, 50 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 52 |  | simp3l 1201 | . . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) | 
| 53 | 52 | sseld 3981 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢)))) | 
| 54 |  | simp1l 1197 | . . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥)) | 
| 55 |  | rankf 9835 | . . . . . . . . . . . . . . . . . . 19
⊢
rank:∪ (𝑅1 “
On)⟶On | 
| 56 |  | ffn 6735 | . . . . . . . . . . . . . . . . . . 19
⊢
(rank:∪ (𝑅1 “
On)⟶On → rank Fn ∪
(𝑅1 “ On)) | 
| 57 | 55, 56 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢ rank Fn
∪ (𝑅1 “
On) | 
| 58 |  | r1tr 9817 | . . . . . . . . . . . . . . . . . . . 20
⊢ Tr
(𝑅1‘𝑥) | 
| 59 |  | trel 5267 | . . . . . . . . . . . . . . . . . . . 20
⊢ (Tr
(𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))) | 
| 60 | 58, 59 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)) | 
| 61 |  | r1elwf 9837 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈
(𝑅1‘𝑥) → 𝑢 ∈ ∪
(𝑅1 “ On)) | 
| 62 |  | tcwf 9924 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ∈ ∪ (𝑅1 “ On)) | 
| 63 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(TC‘𝑢) ∈
V | 
| 64 | 63 | r1elss 9847 | . . . . . . . . . . . . . . . . . . . 20
⊢
((TC‘𝑢) ∈
∪ (𝑅1 “ On) ↔
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) | 
| 65 | 62, 64 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) | 
| 66 | 60, 61, 65 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) | 
| 67 |  | fvelimab 6980 | . . . . . . . . . . . . . . . . . 18
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑢)) ↔
∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤)) | 
| 68 | 57, 66, 67 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤)) | 
| 69 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑧 ∈ V | 
| 70 | 69 | tcel 9786 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧)) | 
| 71 |  | ssrexv 4052 | . . . . . . . . . . . . . . . . . . 19
⊢
((TC‘𝑢)
⊆ (TC‘𝑧) →
(∃𝑥 ∈
(TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 72 | 70, 71 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 73 | 72 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 74 | 68, 73 | sylbid 240 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 75 | 44, 54, 74 | syl2anc 584 | . . . . . . . . . . . . . . 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 9836 | . . . . . . . . . . . . . . . . . . 19
⊢
(rank‘𝑢)
∈ On | 
| 78 |  | eloni 6393 | . . . . . . . . . . . . . . . . . . . 20
⊢
((rank‘𝑢)
∈ On → Ord (rank‘𝑢)) | 
| 79 |  | eloni 6393 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ On → Ord 𝑤) | 
| 80 |  | ordtri3or 6415 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((Ord
(rank‘𝑢) ∧ Ord
𝑤) →
((rank‘𝑢) ∈
𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) | 
| 81 | 78, 79, 80 | syl2an 596 | . . . . . . . . . . . . . . . . . . 19
⊢
(((rank‘𝑢)
∈ On ∧ 𝑤 ∈
On) → ((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) | 
| 82 | 77, 31, 81 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) | 
| 83 |  | 3orass 1089 | . . . . . . . . . . . . . . . . . 18
⊢
(((rank‘𝑢)
∈ 𝑤 ∨
(rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) | 
| 84 | 82, 83 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))) | 
| 85 | 84 | orcanai 1004 | . . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) | 
| 86 | 85 | ad2ant2l 746 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈
(𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))) | 
| 87 | 86 | 3adant2 1131 | . . . . . . . . . . . . . 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 3158 | . . . . . . . . . . . 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 456 | . . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 92 |  | tcwf 9924 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) →
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) | 
| 93 |  | r1elssi 9846 | . . . . . . . . . . . . . 14
⊢
((TC‘𝑧) ∈
∪ (𝑅1 “ On) →
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) | 
| 94 |  | fvelimab 6980 | . . . . . . . . . . . . . 14
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 95 | 93, 94 | sylan2 593 | . . . . . . . . . . . . 13
⊢ ((rank Fn
∪ (𝑅1 “ On) ∧
(TC‘𝑧) ∈ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 96 | 57, 92, 95 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank “
(TC‘𝑧)) ↔
∃𝑥 ∈
(TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 97 | 21, 96 | syl 17 | . . . . . . . . . . 11
⊢ (𝑧 ∈
(𝑅1‘𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 98 | 97 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)) | 
| 99 | 91, 98 | sylibrd 259 | . . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧)))) | 
| 100 | 99 | ssrdv 3988 | . . . . . . . 8
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “
(TC‘𝑧))) | 
| 101 | 100 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈
(𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))) | 
| 102 | 101 | ex 412 | . . . . . 6
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈
(𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))) | 
| 103 | 10, 12, 102 | tfis3 7880 | . . . . 5
⊢ (suc
𝑦 ∈ On →
∀𝑧 ∈
(𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))) | 
| 104 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴)) | 
| 105 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴)) | 
| 106 | 105 | imaeq2d 6077 | . . . . . . 7
⊢ (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “
(TC‘𝐴))) | 
| 107 | 104, 106 | sseq12d 4016 | . . . . . 6
⊢ (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “
(TC‘𝐴)))) | 
| 108 | 107 | rspccv 3618 | . . . . 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 3147 | . . 3
⊢
(∃𝑦 ∈ On
𝐴 ∈
(𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))) | 
| 111 | 1, 110 | sylbi 217 | . 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) ⊆
(rank “ (TC‘𝐴))) | 
| 112 |  | tcvalg 9779 | . . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) = ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)}) | 
| 113 |  | r1rankidb 9845 | . . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆
(𝑅1‘(rank‘𝐴))) | 
| 114 |  | r1tr 9817 | . . . . 5
⊢ Tr
(𝑅1‘(rank‘𝐴)) | 
| 115 |  | fvex 6918 | . . . . . . 7
⊢
(𝑅1‘(rank‘𝐴)) ∈ V | 
| 116 |  | sseq2 4009 | . . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆
(𝑅1‘(rank‘𝐴)))) | 
| 117 |  | treq 5266 | . . . . . . . 8
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr
(𝑅1‘(rank‘𝐴)))) | 
| 118 | 116, 117 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 =
(𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))))) | 
| 119 | 115, 118 | elab 3678 | . . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴)))) | 
| 120 |  | intss1 4962 | . . . . . 6
⊢
((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) | 
| 121 | 119, 120 | sylbir 235 | . . . . 5
⊢ ((𝐴 ⊆
(𝑅1‘(rank‘𝐴)) ∧ Tr
(𝑅1‘(rank‘𝐴))) → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) | 
| 122 | 113, 114,
121 | sylancl 586 | . . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆
(𝑅1‘(rank‘𝐴))) | 
| 123 | 112, 122 | eqsstrd 4017 | . . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(TC‘𝐴) ⊆
(𝑅1‘(rank‘𝐴))) | 
| 124 |  | imass2 6119 | . . . 4
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “
(𝑅1‘(rank‘𝐴)))) | 
| 125 |  | ffun 6738 | . . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) | 
| 126 | 55, 125 | ax-mp 5 | . . . . . . 7
⊢ Fun
rank | 
| 127 |  | fvelima 6973 | . . . . . . 7
⊢ ((Fun
rank ∧ 𝑥 ∈ (rank
“ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) | 
| 128 | 126, 127 | mpan 690 | . . . . . 6
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥) | 
| 129 |  | rankr1ai 9839 | . . . . . . . 8
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴)) | 
| 130 |  | eleq1 2828 | . . . . . . . 8
⊢
((rank‘𝑦) =
𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴))) | 
| 131 | 129, 130 | syl5ibcom 245 | . . . . . . 7
⊢ (𝑦 ∈
(𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))) | 
| 132 | 131 | rexlimiv 3147 | . . . . . 6
⊢
(∃𝑦 ∈
(𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)) | 
| 133 | 128, 132 | syl 17 | . . . . 5
⊢ (𝑥 ∈ (rank “
(𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴)) | 
| 134 | 133 | ssriv 3986 | . . . 4
⊢ (rank
“ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴) | 
| 135 | 124, 134 | sstrdi 3995 | . . 3
⊢
((TC‘𝐴)
⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴)) | 
| 136 | 123, 135 | syl 17 | . 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “
(TC‘𝐴)) ⊆
(rank‘𝐴)) | 
| 137 | 111, 136 | eqssd 4000 | 1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) = (rank
“ (TC‘𝐴))) |