MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tcrank Structured version   Visualization version   GIF version
Theorem tcrank 9852
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 9761 . . 3 (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2 onsuc 7805 . . . . 5 (𝑦 ∈ On → suc 𝑦 ∈ On)
3 fveq2 6881 . . . . . . . 8 (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
43raleqdv 3323 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5 fveq2 6881 . . . . . . . . 9 (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6 fveq2 6881 . . . . . . . . . 10 (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
76imaeq2d 6062 . . . . . . . . 9 (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
85, 7sseq12d 3970 . . . . . . . 8 (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
98cbvralvw 3243 . . . . . . 7 (∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
104, 9bitrdi 290 . . . . . 6 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11 fveq2 6881 . . . . . . 7 (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
1211raleqdv 3323 . . . . . 6 (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
13 simpr 489 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)))
14 simprl 782 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1‘𝑥))
15 simplr 780 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
16 rankr1ai 9766 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥)
17 fveq2 6881 . . . . . . . . . . . . . . . . . 18 (𝑦 = (rank‘𝑧) → (𝑅1‘𝑦) = (𝑅1‘(rank‘𝑧)))
1817raleqdv 3323 . . . . . . . . . . . . . . . . 17 (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
1918rspcv 3577 . . . . . . . . . . . . . . . 16 ((rank‘𝑧) ∈ 𝑥 → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2016, 19syl 18 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1‘𝑥) → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
21 r1elwf 9764 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1‘𝑥) → 𝑧 ∈ ∪ (𝑅1 “ On))
22 r1rankidb 9772 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆ (𝑅1‘(rank‘𝑧)))
23 ssralv 4006 . . . . . . . . . . . . . . . 16 (𝑧 ⊆ (𝑅1‘(rank‘𝑧)) → (∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2421, 22, 233syl 19 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑅1‘𝑥) → (∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2520, 24syld 48 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑅1‘𝑥) → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
2614, 15, 25sylc 66 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
27 rankval3b 9794 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ∪ (𝑅1 “ On) → (rank‘𝑧) = ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})
2827eleq2d 2849 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
2928biimpd 232 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
30 rankon 9763 . . . . . . . . . . . . . . . . . . . 20 (rank‘𝑧) ∈ On
3130oneli 6476 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32 eleq2w 2847 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
3332ralbidv 3188 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
3433onnminsb 7794 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ On → (𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
3531, 34syl 18 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (rank‘𝑧) → (𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
3629, 35sylcom 31 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
3721, 36syl 18 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1‘𝑥) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
3837imp 411 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)
39 rexnal 3117 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)
4038, 39sylibr 237 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
4140adantl 486 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42 r19.29 3128 . . . . . . . . . . . . 13 ((∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
4326, 41, 42syl2anc 595 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
44 simp2 1155 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢 ∈ 𝑧)
45 tcid 9702 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
4645elv 3460 . . . . . . . . . . . . . . . 16 𝑧 ⊆ (TC‘𝑧)
4746sseli 3933 . . . . . . . . . . . . . . 15 (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧))
48 fveqeq2 6890 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
4948rspcev 3581 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
5049ex 417 . . . . . . . . . . . . . . 15 (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
5144, 47, 503syl 19 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
52 simp3l 1220 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
5352sseld 3936 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢))))
54 simp1l 1216 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥))
55 rankf 9762 . . . . . . . . . . . . . . . . . . 19 rank:∪ (𝑅1 “ On)⟶On
56 ffn 6705 . . . . . . . . . . . . . . . . . . 19 (rank:∪ (𝑅1 “ On)⟶On → rank Fn ∪ (𝑅1 “ On))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . 18 rank Fn ∪ (𝑅1 “ On)
58 r1tr 9744 . . . . . . . . . . . . . . . . . . . 20 Tr (𝑅1‘𝑥)
59 trel 5226 . . . . . . . . . . . . . . . . . . . 20 (Tr (𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)))
6058, 59ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))
61 r1elwf 9764 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝑅1‘𝑥) → 𝑢 ∈ ∪ (𝑅1 “ On))
62 tcwf 9851 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ∪ (𝑅1 “ On) → (TC‘𝑢) ∈ ∪ (𝑅1 “ On))
63 fvex 6894 . . . . . . . . . . . . . . . . . . . . 21 (TC‘𝑢) ∈ V
6463r1elss 9774 . . . . . . . . . . . . . . . . . . . 20 ((TC‘𝑢) ∈ ∪ (𝑅1 “ On) ↔ (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
6562, 64sylib 221 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ∪ (𝑅1 “ On) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
6660, 61, 653syl 19 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
67 fvelimab 6953 . . . . . . . . . . . . . . . . . 18 ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
6857, 66, 67sylancr 598 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
69 vex 3459 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
7069tcel 9708 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71 ssrexv 4007 . . . . . . . . . . . . . . . . . . 19 ((TC‘𝑢) ⊆ (TC‘𝑧) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7270, 71syl 18 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ 𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7372adantr 485 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7468, 73sylbid 243 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7544, 54, 74syl2anc 595 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7653, 75syld 48 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
77 rankon 9763 . . . . . . . . . . . . . . . . . . 19 (rank‘𝑢) ∈ On
78 eloni 6370 . . . . . . . . . . . . . . . . . . . 20 ((rank‘𝑢) ∈ On → Ord (rank‘𝑢))
79 eloni 6370 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ On → Ord 𝑤)
80 ordtri3or 6393 . . . . . . . . . . . . . . . . . . . 20 ((Ord (rank‘𝑢) ∧ Ord 𝑤) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
8178, 79, 80syl2an 607 . . . . . . . . . . . . . . . . . . 19 (((rank‘𝑢) ∈ On ∧ 𝑤 ∈ On) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
8277, 31, 81sylancr 598 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
83 3orass 1106 . . . . . . . . . . . . . . . . . 18 (((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))))
8482, 83sylib 221 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))))
8584orcanai 1018 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
8685ad2ant2l 758 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
87863adant2 1149 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
8851, 76, 87mpjaod 873 . . . . . . . . . . . . 13 (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
8988rexlimdv3a 3170 . . . . . . . . . . . 12 ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9013, 43, 89sylc 66 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
9190expr 461 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
92 tcwf 9851 . . . . . . . . . . . . 13 (𝑧 ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ∈ ∪ (𝑅1 “ On))
93 r1elssi 9773 . . . . . . . . . . . . . 14 ((TC‘𝑧) ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ⊆ ∪ (𝑅1 “ On))
94 fvelimab 6953 . . . . . . . . . . . . . 14 ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9593, 94sylan2 604 . . . . . . . . . . . . 13 ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑧) ∈ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9657, 92, 95sylancr 598 . . . . . . . . . . . 12 (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9721, 96syl 18 . . . . . . . . . . 11 (𝑧 ∈ (𝑅1‘𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9897adantl 486 . . . . . . . . . 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 3943 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101100ralrimiva 3157 . . . . . . 7 ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
102101ex 417 . . . . . 6 (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
10310, 12, 102tfis3 7850 . . . . 5 (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104 fveq2 6881 . . . . . . 7 (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105 fveq2 6881 . . . . . . . 8 (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106105imaeq2d 6062 . . . . . . 7 (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107104, 106sseq12d 3970 . . . . . 6 (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108107rspccv 3578 . . . . 5 (∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
1092, 103, 1083syl 19 . . . 4 (𝑦 ∈ On → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
110109rexlimiv 3159 . . 3 (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
1111, 110sylbi 220 . 2 (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
112 tcvalg 9701 . . . 4 (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)})
113 r1rankidb 9772 . . . . 5 (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
114 r1tr 9744 . . . . 5 Tr (𝑅1‘(rank‘𝐴))
115 fvex 6894 . . . . . . 7 (𝑅1‘(rank‘𝐴)) ∈ V
116 sseq2 3963 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (𝑅1‘(rank‘𝐴))))
117 treq 5225 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr (𝑅1‘(rank‘𝐴))))
118116, 117anbi12d 643 . . . . . . 7 (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119115, 118elab 3638 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120 intss1 4928 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
121119, 120sylbir 238 . . . . 5 ((𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))) → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
122113, 114, 121sylancl 597 . . . 4 (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
123112, 122eqsstrd 3971 . . 3 (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)))
124 imass2 6104 . . . 4 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “ (𝑅1‘(rank‘𝐴))))
125 ffun 6708 . . . . . . . 8 (rank:∪ (𝑅1 “ On)⟶On → Fun rank)
12655, 125ax-mp 5 . . . . . . 7 Fun rank
127 fvelima 6946 . . . . . . 7 ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128126, 127mpan 702 . . . . . 6 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129 rankr1ai 9766 . . . . . . . 8 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130 eleq1 2851 . . . . . . . 8 ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131129, 130syl5ibcom 248 . . . . . . 7 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)))
132131rexlimiv 3159 . . . . . 6 (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))
133128, 132syl 18 . . . . 5 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134133ssriv 3941 . . . 4 (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135124, 134sstrdi 3949 . . 3 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136123, 135syl 18 . 2 (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137111, 136eqssd 3954 1 (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  {cab 2741  ∀wral 3079  ∃wrex 3089  {crab 3416  Vcvv 3455   ⊆ wss 3905  ∪ cuni 4872  ∩ cint 4912  Tr wtr 5218   “ cima 5664  Ord word 6359  Oncon0 6360  suc csuc 6362  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  TCctc 9699  𝑅1cr1 9730  rankcrnk 9731
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606
This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-tc 9700  df-r1 9732  df-rank 9733
This theorem is used by:  hsmexlem5  10418  grur1  10809
  Copyright terms: Public domain W3C validator