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

Theorem tcrank 8997
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 8906 . . 3 (𝐴 (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2 suceloni 7246 . . . . 5 (𝑦 ∈ On → suc 𝑦 ∈ On)
3 fveq2 6411 . . . . . . . 8 (𝑥 = 𝑦 → (𝑅1𝑥) = (𝑅1𝑦))
43raleqdv 3340 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5 fveq2 6411 . . . . . . . . 9 (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6 fveq2 6411 . . . . . . . . . 10 (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
76imaeq2d 5683 . . . . . . . . 9 (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
85, 7sseq12d 3838 . . . . . . . 8 (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
98cbvralv 3367 . . . . . . 7 (∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
104, 9syl6bb 278 . . . . . 6 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11 fveq2 6411 . . . . . . 7 (𝑥 = suc 𝑦 → (𝑅1𝑥) = (𝑅1‘suc 𝑦))
1211raleqdv 3340 . . . . . 6 (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
13 simpr 473 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)))
14 simprl 778 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1𝑥))
15 simplr 776 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
16 rankr1ai 8911 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1𝑥) → (rank‘𝑧) ∈ 𝑥)
17 fveq2 6411 . . . . . . . . . . . . . . . . . 18 (𝑦 = (rank‘𝑧) → (𝑅1𝑦) = (𝑅1‘(rank‘𝑧)))
1817raleqdv 3340 . . . . . . . . . . . . . . . . 17 (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
1918rspcv 3505 . . . . . . . . . . . . . . . 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 8909 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1𝑥) → 𝑧 (𝑅1 “ On))
22 r1rankidb 8917 . . . . . . . . . . . . . . . 16 (𝑧 (𝑅1 “ On) → 𝑧 ⊆ (𝑅1‘(rank‘𝑧)))
23 ssralv 3870 . . . . . . . . . . . . . . . 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 8939 . . . . . . . . . . . . . . . . . . . 20 (𝑧 (𝑅1 “ On) → (rank‘𝑧) = {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥})
2827eleq2d 2878 . . . . . . . . . . . . . . . . . . 19 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
2928biimpd 220 . . . . . . . . . . . . . . . . . 18 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
30 rankon 8908 . . . . . . . . . . . . . . . . . . . 20 (rank‘𝑧) ∈ On
3130oneli 6051 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32 eleq2w 2876 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
3332ralbidv 3181 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3433onnminsb 7237 . . . . . . . . . . . . . . . . . . 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 395 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤)
39 rexnal 3189 . . . . . . . . . . . . . . 15 (∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤)
4038, 39sylibr 225 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
4140adantl 469 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42 r19.29 3267 . . . . . . . . . . . . 13 ((∀𝑢𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
4326, 41, 42syl2anc 575 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
44 simp2 1160 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢𝑧)
45 vex 3401 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
46 tcid 8865 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
4745, 46ax-mp 5 . . . . . . . . . . . . . . . 16 𝑧 ⊆ (TC‘𝑧)
4847sseli 3801 . . . . . . . . . . . . . . 15 (𝑢𝑧𝑢 ∈ (TC‘𝑧))
49 fveqeq2 6420 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
5049rspcev 3509 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
5150ex 399 . . . . . . . . . . . . . . 15 (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
5244, 48, 513syl 18 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
53 simp3l 1251 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
5453sseld 3804 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢))))
55 simp1l 1247 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1𝑥))
56 rankf 8907 . . . . . . . . . . . . . . . . . . 19 rank: (𝑅1 “ On)⟶On
57 ffn 6259 . . . . . . . . . . . . . . . . . . 19 (rank: (𝑅1 “ On)⟶On → rank Fn (𝑅1 “ On))
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . 18 rank Fn (𝑅1 “ On)
59 r1tr 8889 . . . . . . . . . . . . . . . . . . . 20 Tr (𝑅1𝑥)
60 trel 4960 . . . . . . . . . . . . . . . . . . . 20 (Tr (𝑅1𝑥) → ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → 𝑢 ∈ (𝑅1𝑥)))
6159, 60ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → 𝑢 ∈ (𝑅1𝑥))
62 r1elwf 8909 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝑅1𝑥) → 𝑢 (𝑅1 “ On))
63 tcwf 8996 . . . . . . . . . . . . . . . . . . . 20 (𝑢 (𝑅1 “ On) → (TC‘𝑢) ∈ (𝑅1 “ On))
64 fvex 6424 . . . . . . . . . . . . . . . . . . . . 21 (TC‘𝑢) ∈ V
6564r1elss 8919 . . . . . . . . . . . . . . . . . . . 20 ((TC‘𝑢) ∈ (𝑅1 “ On) ↔ (TC‘𝑢) ⊆ (𝑅1 “ On))
6663, 65sylib 209 . . . . . . . . . . . . . . . . . . 19 (𝑢 (𝑅1 “ On) → (TC‘𝑢) ⊆ (𝑅1 “ On))
6761, 62, 663syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (TC‘𝑢) ⊆ (𝑅1 “ On))
68 fvelimab 6477 . . . . . . . . . . . . . . . . . 18 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
6958, 67, 68sylancr 577 . . . . . . . . . . . . . . . . 17 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
7045tcel 8871 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71 ssrexv 3871 . . . . . . . . . . . . . . . . . . 19 ((TC‘𝑢) ⊆ (TC‘𝑧) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7270, 71syl 17 . . . . . . . . . . . . . . . . . 18 (𝑢𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7372adantr 468 . . . . . . . . . . . . . . . . 17 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7469, 73sylbid 231 . . . . . . . . . . . . . . . 16 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7544, 55, 74syl2anc 575 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7654, 75syld 47 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
77 rankon 8908 . . . . . . . . . . . . . . . . . . 19 (rank‘𝑢) ∈ On
78 eloni 5953 . . . . . . . . . . . . . . . . . . . 20 ((rank‘𝑢) ∈ On → Ord (rank‘𝑢))
79 eloni 5953 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ On → Ord 𝑤)
80 ordtri3or 5975 . . . . . . . . . . . . . . . . . . . 20 ((Ord (rank‘𝑢) ∧ Ord 𝑤) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8178, 79, 80syl2an 585 . . . . . . . . . . . . . . . . . . 19 (((rank‘𝑢) ∈ On ∧ 𝑤 ∈ On) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8277, 31, 81sylancr 577 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
83 3orass 1103 . . . . . . . . . . . . . . . . . 18 (((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8482, 83sylib 209 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8584orcanai 1016 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8685ad2ant2l 743 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
87863adant2 1154 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8852, 76, 87mpjaod 878 . . . . . . . . . . . . 13 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
8988rexlimdv3a 3228 . . . . . . . . . . . 12 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9013, 43, 89sylc 65 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
9190expr 446 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
92 tcwf 8996 . . . . . . . . . . . . 13 (𝑧 (𝑅1 “ On) → (TC‘𝑧) ∈ (𝑅1 “ On))
93 r1elssi 8918 . . . . . . . . . . . . . 14 ((TC‘𝑧) ∈ (𝑅1 “ On) → (TC‘𝑧) ⊆ (𝑅1 “ On))
94 fvelimab 6477 . . . . . . . . . . . . . 14 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑧) ⊆ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9593, 94sylan2 582 . . . . . . . . . . . . 13 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑧) ∈ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9658, 92, 95sylancr 577 . . . . . . . . . . . 12 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9721, 96syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝑅1𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9897adantl 469 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9991, 98sylibrd 250 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧))))
10099ssrdv 3811 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101100ralrimiva 3161 . . . . . . 7 ((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
102101ex 399 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
10310, 12, 102tfis3 7290 . . . . 5 (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104 fveq2 6411 . . . . . . 7 (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105 fveq2 6411 . . . . . . . 8 (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106105imaeq2d 5683 . . . . . . 7 (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107104, 106sseq12d 3838 . . . . . 6 (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108107rspccv 3506 . . . . 5 (∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
1092, 103, 1083syl 18 . . . 4 (𝑦 ∈ On → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
110109rexlimiv 3222 . . 3 (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
1111, 110sylbi 208 . 2 (𝐴 (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
112 tcvalg 8864 . . . 4 (𝐴 (𝑅1 “ On) → (TC‘𝐴) = {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)})
113 r1rankidb 8917 . . . . 5 (𝐴 (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
114 r1tr 8889 . . . . 5 Tr (𝑅1‘(rank‘𝐴))
115 fvex 6424 . . . . . . 7 (𝑅1‘(rank‘𝐴)) ∈ V
116 sseq2 3831 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (𝐴𝑥𝐴 ⊆ (𝑅1‘(rank‘𝐴))))
117 treq 4959 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr (𝑅1‘(rank‘𝐴))))
118116, 117anbi12d 618 . . . . . . 7 (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119115, 118elab 3552 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120 intss1 4691 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
121119, 120sylbir 226 . . . . 5 ((𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))) → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
122113, 114, 121sylancl 576 . . . 4 (𝐴 (𝑅1 “ On) → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
123112, 122eqsstrd 3843 . . 3 (𝐴 (𝑅1 “ On) → (TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)))
124 imass2 5718 . . . 4 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “ (𝑅1‘(rank‘𝐴))))
125 ffun 6262 . . . . . . . 8 (rank: (𝑅1 “ On)⟶On → Fun rank)
12656, 125ax-mp 5 . . . . . . 7 Fun rank
127 fvelima 6472 . . . . . . 7 ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128126, 127mpan 673 . . . . . 6 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129 rankr1ai 8911 . . . . . . . 8 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130 eleq1 2880 . . . . . . . 8 ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131129, 130syl5ibcom 236 . . . . . . 7 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴)))
132131rexlimiv 3222 . . . . . 6 (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴))
133128, 132syl 17 . . . . 5 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134133ssriv 3809 . . . 4 (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135124, 134syl6ss 3817 . . 3 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136123, 135syl 17 . 2 (𝐴 (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137111, 136eqssd 3822 1 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3o 1099  w3a 1100   = wceq 1637  wcel 2157  {cab 2799  wral 3103  wrex 3104  {crab 3107  Vcvv 3398  wss 3776   cuni 4637   cint 4676  Tr wtr 4953  cima 5321  Ord word 5942  Oncon0 5943  suc csuc 5945  Fun wfun 6098   Fn wfn 6099  wf 6100  cfv 6104  TCctc 8862  𝑅1cr1 8875  rankcrnk 8876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-om 7299  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-tc 8863  df-r1 8877  df-rank 8878
This theorem is referenced by:  hsmexlem5  9540  grur1  9930
  Copyright terms: Public domain W3C validator