MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tcrank Structured version   Visualization version   GIF version

Theorem tcrank 9301
Description: This theorem expresses two different facts from the two subset implications in this equality. In the forward direction, it says that the transitive closure has members of every rank below 𝐴. Stated another way, to construct a set at a given rank, you have to climb the entire hierarchy of ordinals below (rank‘𝐴), constructing at least one set at each level in order to move up the ranks. In the reverse direction, it says that every member of (TC‘𝐴) has a rank below the rank of 𝐴, since intuitively it contains only the members of 𝐴 and the members of those and so on, but nothing "bigger" than 𝐴. (Contributed by Mario Carneiro, 23-Jun-2013.)
Assertion
Ref Expression
tcrank (𝐴 (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))

Proof of Theorem tcrank
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rankwflemb 9210 . . 3 (𝐴 (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2 suceloni 7512 . . . . 5 (𝑦 ∈ On → suc 𝑦 ∈ On)
3 fveq2 6649 . . . . . . . 8 (𝑥 = 𝑦 → (𝑅1𝑥) = (𝑅1𝑦))
43raleqdv 3367 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5 fveq2 6649 . . . . . . . . 9 (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6 fveq2 6649 . . . . . . . . . 10 (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
76imaeq2d 5900 . . . . . . . . 9 (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
85, 7sseq12d 3951 . . . . . . . 8 (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
98cbvralvw 3399 . . . . . . 7 (∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
104, 9syl6bb 290 . . . . . 6 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11 fveq2 6649 . . . . . . 7 (𝑥 = suc 𝑦 → (𝑅1𝑥) = (𝑅1‘suc 𝑦))
1211raleqdv 3367 . . . . . 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 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 9215 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1𝑥) → (rank‘𝑧) ∈ 𝑥)
17 fveq2 6649 . . . . . . . . . . . . . . . . . 18 (𝑦 = (rank‘𝑧) → (𝑅1𝑦) = (𝑅1‘(rank‘𝑧)))
1817raleqdv 3367 . . . . . . . . . . . . . . . . 17 (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
1918rspcv 3569 . . . . . . . . . . . . . . . 16 ((rank‘𝑧) ∈ 𝑥 → (∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2016, 19syl 17 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1𝑥) → (∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
21 r1elwf 9213 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1𝑥) → 𝑧 (𝑅1 “ On))
22 r1rankidb 9221 . . . . . . . . . . . . . . . 16 (𝑧 (𝑅1 “ On) → 𝑧 ⊆ (𝑅1‘(rank‘𝑧)))
23 ssralv 3984 . . . . . . . . . . . . . . . 16 (𝑧 ⊆ (𝑅1‘(rank‘𝑧)) → (∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2421, 22, 233syl 18 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1𝑥) → (∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2520, 24syld 47 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1𝑥) → (∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2614, 15, 25sylc 65 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑢𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
27 rankval3b 9243 . . . . . . . . . . . . . . . . . . . 20 (𝑧 (𝑅1 “ On) → (rank‘𝑧) = {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥})
2827eleq2d 2878 . . . . . . . . . . . . . . . . . . 19 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
2928biimpd 232 . . . . . . . . . . . . . . . . . 18 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
30 rankon 9212 . . . . . . . . . . . . . . . . . . . 20 (rank‘𝑧) ∈ On
3130oneli 6270 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32 eleq2w 2876 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
3332ralbidv 3165 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3433onnminsb 7503 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ On → (𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3531, 34syl 17 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (rank‘𝑧) → (𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3629, 35sylcom 30 . . . . . . . . . . . . . . . . 17 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3721, 36syl 17 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1𝑥) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3837imp 410 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤)
39 rexnal 3204 . . . . . . . . . . . . . . 15 (∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤)
4038, 39sylibr 237 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
4140adantl 485 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42 r19.29 3219 . . . . . . . . . . . . 13 ((∀𝑢𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
4326, 41, 42syl2anc 587 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
44 simp2 1134 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢𝑧)
45 tcid 9169 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
4645elv 3449 . . . . . . . . . . . . . . . 16 𝑧 ⊆ (TC‘𝑧)
4746sseli 3914 . . . . . . . . . . . . . . 15 (𝑢𝑧𝑢 ∈ (TC‘𝑧))
48 fveqeq2 6658 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
4948rspcev 3574 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
5049ex 416 . . . . . . . . . . . . . . 15 (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
5144, 47, 503syl 18 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
52 simp3l 1198 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
5352sseld 3917 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢))))
54 simp1l 1194 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1𝑥))
55 rankf 9211 . . . . . . . . . . . . . . . . . . 19 rank: (𝑅1 “ On)⟶On
56 ffn 6491 . . . . . . . . . . . . . . . . . . 19 (rank: (𝑅1 “ On)⟶On → rank Fn (𝑅1 “ On))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . 18 rank Fn (𝑅1 “ On)
58 r1tr 9193 . . . . . . . . . . . . . . . . . . . 20 Tr (𝑅1𝑥)
59 trel 5146 . . . . . . . . . . . . . . . . . . . 20 (Tr (𝑅1𝑥) → ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → 𝑢 ∈ (𝑅1𝑥)))
6058, 59ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → 𝑢 ∈ (𝑅1𝑥))
61 r1elwf 9213 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝑅1𝑥) → 𝑢 (𝑅1 “ On))
62 tcwf 9300 . . . . . . . . . . . . . . . . . . . 20 (𝑢 (𝑅1 “ On) → (TC‘𝑢) ∈ (𝑅1 “ On))
63 fvex 6662 . . . . . . . . . . . . . . . . . . . . 21 (TC‘𝑢) ∈ V
6463r1elss 9223 . . . . . . . . . . . . . . . . . . . 20 ((TC‘𝑢) ∈ (𝑅1 “ On) ↔ (TC‘𝑢) ⊆ (𝑅1 “ On))
6562, 64sylib 221 . . . . . . . . . . . . . . . . . . 19 (𝑢 (𝑅1 “ On) → (TC‘𝑢) ⊆ (𝑅1 “ On))
6660, 61, 653syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (TC‘𝑢) ⊆ (𝑅1 “ On))
67 fvelimab 6716 . . . . . . . . . . . . . . . . . 18 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
6857, 66, 67sylancr 590 . . . . . . . . . . . . . . . . 17 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
69 vex 3447 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
7069tcel 9175 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71 ssrexv 3985 . . . . . . . . . . . . . . . . . . 19 ((TC‘𝑢) ⊆ (TC‘𝑧) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7270, 71syl 17 . . . . . . . . . . . . . . . . . 18 (𝑢𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7372adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7468, 73sylbid 243 . . . . . . . . . . . . . . . 16 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7544, 54, 74syl2anc 587 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7653, 75syld 47 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
77 rankon 9212 . . . . . . . . . . . . . . . . . . 19 (rank‘𝑢) ∈ On
78 eloni 6173 . . . . . . . . . . . . . . . . . . . 20 ((rank‘𝑢) ∈ On → Ord (rank‘𝑢))
79 eloni 6173 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ On → Ord 𝑤)
80 ordtri3or 6195 . . . . . . . . . . . . . . . . . . . 20 ((Ord (rank‘𝑢) ∧ Ord 𝑤) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8178, 79, 80syl2an 598 . . . . . . . . . . . . . . . . . . 19 (((rank‘𝑢) ∈ On ∧ 𝑤 ∈ On) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8277, 31, 81sylancr 590 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
83 3orass 1087 . . . . . . . . . . . . . . . . . 18 (((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8482, 83sylib 221 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8584orcanai 1000 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8685ad2ant2l 745 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
87863adant2 1128 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8851, 76, 87mpjaod 857 . . . . . . . . . . . . 13 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
8988rexlimdv3a 3248 . . . . . . . . . . . 12 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9013, 43, 89sylc 65 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
9190expr 460 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
92 tcwf 9300 . . . . . . . . . . . . 13 (𝑧 (𝑅1 “ On) → (TC‘𝑧) ∈ (𝑅1 “ On))
93 r1elssi 9222 . . . . . . . . . . . . . 14 ((TC‘𝑧) ∈ (𝑅1 “ On) → (TC‘𝑧) ⊆ (𝑅1 “ On))
94 fvelimab 6716 . . . . . . . . . . . . . 14 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑧) ⊆ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9593, 94sylan2 595 . . . . . . . . . . . . 13 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑧) ∈ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9657, 92, 95sylancr 590 . . . . . . . . . . . 12 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9721, 96syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝑅1𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9897adantl 485 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9991, 98sylibrd 262 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧))))
10099ssrdv 3924 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101100ralrimiva 3152 . . . . . . 7 ((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
102101ex 416 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
10310, 12, 102tfis3 7556 . . . . 5 (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104 fveq2 6649 . . . . . . 7 (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105 fveq2 6649 . . . . . . . 8 (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106105imaeq2d 5900 . . . . . . 7 (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107104, 106sseq12d 3951 . . . . . 6 (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108107rspccv 3571 . . . . 5 (∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
1092, 103, 1083syl 18 . . . 4 (𝑦 ∈ On → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
110109rexlimiv 3242 . . 3 (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
1111, 110sylbi 220 . 2 (𝐴 (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
112 tcvalg 9168 . . . 4 (𝐴 (𝑅1 “ On) → (TC‘𝐴) = {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)})
113 r1rankidb 9221 . . . . 5 (𝐴 (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
114 r1tr 9193 . . . . 5 Tr (𝑅1‘(rank‘𝐴))
115 fvex 6662 . . . . . . 7 (𝑅1‘(rank‘𝐴)) ∈ V
116 sseq2 3944 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (𝐴𝑥𝐴 ⊆ (𝑅1‘(rank‘𝐴))))
117 treq 5145 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr (𝑅1‘(rank‘𝐴))))
118116, 117anbi12d 633 . . . . . . 7 (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119115, 118elab 3618 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120 intss1 4856 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
121119, 120sylbir 238 . . . . 5 ((𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))) → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
122113, 114, 121sylancl 589 . . . 4 (𝐴 (𝑅1 “ On) → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
123112, 122eqsstrd 3956 . . 3 (𝐴 (𝑅1 “ On) → (TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)))
124 imass2 5936 . . . 4 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “ (𝑅1‘(rank‘𝐴))))
125 ffun 6494 . . . . . . . 8 (rank: (𝑅1 “ On)⟶On → Fun rank)
12655, 125ax-mp 5 . . . . . . 7 Fun rank
127 fvelima 6710 . . . . . . 7 ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128126, 127mpan 689 . . . . . 6 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129 rankr1ai 9215 . . . . . . . 8 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130 eleq1 2880 . . . . . . . 8 ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131129, 130syl5ibcom 248 . . . . . . 7 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴)))
132131rexlimiv 3242 . . . . . 6 (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴))
133128, 132syl 17 . . . . 5 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134133ssriv 3922 . . . 4 (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135124, 134sstrdi 3930 . . 3 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136123, 135syl 17 . 2 (𝐴 (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137111, 136eqssd 3935 1 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3o 1083  w3a 1084   = wceq 1538  wcel 2112  {cab 2779  wral 3109  wrex 3110  {crab 3113  Vcvv 3444  wss 3884   cuni 4803   cint 4841  Tr wtr 5139  cima 5526  Ord word 6162  Oncon0 6163  suc csuc 6165  Fun wfun 6322   Fn wfn 6323  wf 6324  cfv 6328  TCctc 9166  𝑅1cr1 9179  rankcrnk 9180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-tc 9167  df-r1 9181  df-rank 9182
This theorem is referenced by:  hsmexlem5  9845  grur1  10235
  Copyright terms: Public domain W3C validator