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

Theorem tcrank 9513
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 9422 . . 3 (𝐴 (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2 suceloni 7601 . . . . 5 (𝑦 ∈ On → suc 𝑦 ∈ On)
3 fveq2 6726 . . . . . . . 8 (𝑥 = 𝑦 → (𝑅1𝑥) = (𝑅1𝑦))
43raleqdv 3332 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5 fveq2 6726 . . . . . . . . 9 (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6 fveq2 6726 . . . . . . . . . 10 (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
76imaeq2d 5938 . . . . . . . . 9 (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
85, 7sseq12d 3943 . . . . . . . 8 (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
98cbvralvw 3365 . . . . . . 7 (∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
104, 9bitrdi 290 . . . . . 6 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11 fveq2 6726 . . . . . . 7 (𝑥 = suc 𝑦 → (𝑅1𝑥) = (𝑅1‘suc 𝑦))
1211raleqdv 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‘𝑧)))
1817raleqdv 3332 . . . . . . . . . . . . . . . . 17 (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
1918rspcv 3539 . . . . . . . . . . . . . . . 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 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‘𝑢))))
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 9455 . . . . . . . . . . . . . . . . . . . 20 (𝑧 (𝑅1 “ On) → (rank‘𝑧) = {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥})
2827eleq2d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
2928biimpd 232 . . . . . . . . . . . . . . . . . 18 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
30 rankon 9424 . . . . . . . . . . . . . . . . . . . 20 (rank‘𝑧) ∈ On
3130oneli 6330 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32 eleq2w 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
3332ralbidv 3119 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3433onnminsb 7592 . . . . . . . . . . . . . . . . . . 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 3164 . . . . . . . . . . . . . . 15 (∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤)
4038, 39sylibr 237 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
4140adantl 485 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42 r19.29 3182 . . . . . . . . . . . . 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 1139 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢𝑧)
45 tcid 9368 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
4645elv 3421 . . . . . . . . . . . . . . . 16 𝑧 ⊆ (TC‘𝑧)
4746sseli 3905 . . . . . . . . . . . . . . 15 (𝑢𝑧𝑢 ∈ (TC‘𝑧))
48 fveqeq2 6735 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
4948rspcev 3544 . . . . . . . . . . . . . . . 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 1203 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
5352sseld 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))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . 18 rank Fn (𝑅1 “ On)
58 r1tr 9405 . . . . . . . . . . . . . . . . . . . 20 Tr (𝑅1𝑥)
59 trel 5177 . . . . . . . . . . . . . . . . . . . 20 (Tr (𝑅1𝑥) → ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → 𝑢 ∈ (𝑅1𝑥)))
6058, 59ax-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
6463r1elss 9435 . . . . . . . . . . . . . . . . . . . 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 6793 . . . . . . . . . . . . . . . . . 18 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
6857, 66, 67sylancr 590 . . . . . . . . . . . . . . . . 17 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
69 vex 3419 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
7069tcel 9374 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71 ssrexv 3977 . . . . . . . . . . . . . . . . . . 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 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‘𝑢)))
8178, 79, 80syl2an 599 . . . . . . . . . . . . . . . . . . 19 (((rank‘𝑢) ∈ On ∧ 𝑤 ∈ On) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8277, 31, 81sylancr 590 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
83 3orass 1092 . . . . . . . . . . . . . . . . . 18 (((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8482, 83sylib 221 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8584orcanai 1003 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8685ad2ant2l 746 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
87863adant2 1133 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8851, 76, 87mpjaod 860 . . . . . . . . . . . . 13 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
8988rexlimdv3a 3212 . . . . . . . . . . . 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 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‘𝑥) = 𝑤))
9593, 94sylan2 596 . . . . . . . . . . . . 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 3916 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101100ralrimiva 3106 . . . . . . 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 7645 . . . . 5 (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104 fveq2 6726 . . . . . . 7 (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105 fveq2 6726 . . . . . . . 8 (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106105imaeq2d 5938 . . . . . . 7 (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107104, 106sseq12d 3943 . . . . . 6 (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108107rspccv 3541 . . . . 5 (∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
1092, 103, 1083syl 18 . . . 4 (𝑦 ∈ On → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
110109rexlimiv 3206 . . 3 (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
1111, 110sylbi 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‘𝐴))))
118116, 117anbi12d 634 . . . . . . 7 (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119115, 118elab 3594 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120 intss1 4883 . . . . . 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 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)
12655, 125ax-mp 5 . . . . . . 7 Fun rank
127 fvelima 6787 . . . . . . 7 ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128126, 127mpan 690 . . . . . 6 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129 rankr1ai 9427 . . . . . . . 8 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130 eleq1 2826 . . . . . . . 8 ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131129, 130syl5ibcom 248 . . . . . . 7 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴)))
132131rexlimiv 3206 . . . . . 6 (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴))
133128, 132syl 17 . . . . 5 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134133ssriv 3914 . . . 4 (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135124, 134sstrdi 3922 . . 3 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136123, 135syl 17 . 2 (𝐴 (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137111, 136eqssd 3927 1 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3o 1088  w3a 1089   = wceq 1543  wcel 2111  {cab 2715  wral 3062  wrex 3063  {crab 3066  Vcvv 3415  wss 3875   cuni 4828   cint 4868  Tr wtr 5170  cima 5563  Ord word 6221  Oncon0 6222  suc csuc 6224  Fun wfun 6383   Fn wfn 6384  wf 6385  cfv 6389  TCctc 9365  𝑅1cr1 9391  rankcrnk 9392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5188  ax-sep 5201  ax-nul 5208  ax-pow 5267  ax-pr 5331  ax-un 7532  ax-inf2 9269
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-pss 3894  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4829  df-int 4869  df-iun 4915  df-br 5063  df-opab 5125  df-mpt 5145  df-tr 5171  df-id 5464  df-eprel 5469  df-po 5477  df-so 5478  df-fr 5518  df-we 5520  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-pred 6169  df-ord 6225  df-on 6226  df-lim 6227  df-suc 6228  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-om 7654  df-wrecs 8056  df-recs 8117  df-rdg 8155  df-tc 9366  df-r1 9393  df-rank 9394
This theorem is referenced by:  hsmexlem5  10057  grur1  10447
  Copyright terms: Public domain W3C validator