MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tcrank Structured version   Visualization version   GIF version
Theorem tcrank 9465
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 9374 . . 3 (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2 suceloni 7570 . . . . 5 (𝑦 ∈ On → suc 𝑦 ∈ On)
3 fveq2 6695 . . . . . . . 8 (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
43raleqdv 3315 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5 fveq2 6695 . . . . . . . . 9 (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6 fveq2 6695 . . . . . . . . . 10 (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
76imaeq2d 5914 . . . . . . . . 9 (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
85, 7sseq12d 3920 . . . . . . . 8 (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
98cbvralvw 3348 . . . . . . 7 (∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
104, 9bitrdi 290 . . . . . 6 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11 fveq2 6695 . . . . . . 7 (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
1211raleqdv 3315 . . . . . 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 9379 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥)
17 fveq2 6695 . . . . . . . . . . . . . . . . . 18 (𝑦 = (rank‘𝑧) → (𝑅1‘𝑦) = (𝑅1‘(rank‘𝑧)))
1817raleqdv 3315 . . . . . . . . . . . . . . . . 17 (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
1918rspcv 3522 . . . . . . . . . . . . . . . 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 9377 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1‘𝑥) → 𝑧 ∈ ∪ (𝑅1 “ On))
22 r1rankidb 9385 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆ (𝑅1‘(rank‘𝑧)))
23 ssralv 3953 . . . . . . . . . . . . . . . 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 9407 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ∪ (𝑅1 “ On) → (rank‘𝑧) = ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})
2827eleq2d 2816 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
2928biimpd 232 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
30 rankon 9376 . . . . . . . . . . . . . . . . . . . 20 (rank‘𝑧) ∈ On
3130oneli 6299 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32 eleq2w 2814 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
3332ralbidv 3108 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
3433onnminsb 7561 . . . . . . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)
4038, 39sylibr 237 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
4140adantl 485 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42 r19.29 3166 . . . . . . . . . . . . 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 9333 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
4645elv 3404 . . . . . . . . . . . . . . . 16 𝑧 ⊆ (TC‘𝑧)
4746sseli 3883 . . . . . . . . . . . . . . 15 (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧))
48 fveqeq2 6704 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
4948rspcev 3527 . . . . . . . . . . . . . . . 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 3886 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢))))
54 simp1l 1199 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥))
55 rankf 9375 . . . . . . . . . . . . . . . . . . 19 rank:∪ (𝑅1 “ On)⟶On
56 ffn 6523 . . . . . . . . . . . . . . . . . . 19 (rank:∪ (𝑅1 “ On)⟶On → rank Fn ∪ (𝑅1 “ On))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . 18 rank Fn ∪ (𝑅1 “ On)
58 r1tr 9357 . . . . . . . . . . . . . . . . . . . 20 Tr (𝑅1‘𝑥)
59 trel 5153 . . . . . . . . . . . . . . . . . . . 20 (Tr (𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)))
6058, 59ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))
61 r1elwf 9377 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝑅1‘𝑥) → 𝑢 ∈ ∪ (𝑅1 “ On))
62 tcwf 9464 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ∪ (𝑅1 “ On) → (TC‘𝑢) ∈ ∪ (𝑅1 “ On))
63 fvex 6708 . . . . . . . . . . . . . . . . . . . . 21 (TC‘𝑢) ∈ V
6463r1elss 9387 . . . . . . . . . . . . . . . . . . . 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 6762 . . . . . . . . . . . . . . . . . 18 ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
6857, 66, 67sylancr 590 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
69 vex 3402 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
7069tcel 9339 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71 ssrexv 3954 . . . . . . . . . . . . . . . . . . 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 9376 . . . . . . . . . . . . . . . . . . 19 (rank‘𝑢) ∈ On
78 eloni 6201 . . . . . . . . . . . . . . . . . . . 20 ((rank‘𝑢) ∈ On → Ord (rank‘𝑢))
79 eloni 6201 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ On → Ord 𝑤)
80 ordtri3or 6223 . . . . . . . . . . . . . . . . . . . 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 3195 . . . . . . . . . . . 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 9464 . . . . . . . . . . . . 13 (𝑧 ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ∈ ∪ (𝑅1 “ On))
93 r1elssi 9386 . . . . . . . . . . . . . 14 ((TC‘𝑧) ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ⊆ ∪ (𝑅1 “ On))
94 fvelimab 6762 . . . . . . . . . . . . . 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 3893 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101100ralrimiva 3095 . . . . . . 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 7614 . . . . 5 (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104 fveq2 6695 . . . . . . 7 (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105 fveq2 6695 . . . . . . . 8 (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106105imaeq2d 5914 . . . . . . 7 (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107104, 106sseq12d 3920 . . . . . 6 (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108107rspccv 3524 . . . . 5 (∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
1092, 103, 1083syl 18 . . . 4 (𝑦 ∈ On → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
110109rexlimiv 3189 . . 3 (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
1111, 110sylbi 220 . 2 (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
112 tcvalg 9332 . . . 4 (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)})
113 r1rankidb 9385 . . . . 5 (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
114 r1tr 9357 . . . . 5 Tr (𝑅1‘(rank‘𝐴))
115 fvex 6708 . . . . . . 7 (𝑅1‘(rank‘𝐴)) ∈ V
116 sseq2 3913 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (𝑅1‘(rank‘𝐴))))
117 treq 5152 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr (𝑅1‘(rank‘𝐴))))
118116, 117anbi12d 634 . . . . . . 7 (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119115, 118elab 3576 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120 intss1 4860 . . . . . 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 3925 . . 3 (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)))
124 imass2 5950 . . . 4 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “ (𝑅1‘(rank‘𝐴))))
125 ffun 6526 . . . . . . . 8 (rank:∪ (𝑅1 “ On)⟶On → Fun rank)
12655, 125ax-mp 5 . . . . . . 7 Fun rank
127 fvelima 6756 . . . . . . 7 ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128126, 127mpan 690 . . . . . 6 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129 rankr1ai 9379 . . . . . . . 8 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130 eleq1 2818 . . . . . . . 8 ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131129, 130syl5ibcom 248 . . . . . . 7 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)))
132131rexlimiv 3189 . . . . . 6 (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))
133128, 132syl 17 . . . . 5 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134133ssriv 3891 . . . 4 (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135124, 134sstrdi 3899 . . 3 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136123, 135syl 17 . 2 (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137111, 136eqssd 3904 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 2112  {cab 2714  ∀wral 3051  ∃wrex 3052  {crab 3055  Vcvv 3398   ⊆ wss 3853  ∪ cuni 4805  ∩ cint 4845  Tr wtr 5146   “ cima 5539  Ord word 6190  Oncon0 6191  suc csuc 6193  Fun wfun 6352   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  TCctc 9330  𝑅1cr1 9343  rankcrnk 9344
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 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-inf2 9234
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 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-int 4846  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-tc 9331  df-r1 9345  df-rank 9346
This theorem is referenced by:  hsmexlem5  10009  grur1  10399
  Copyright terms: Public domain W3C validator