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

Theorem tcrank 9148
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 9057 . . 3 (𝐴 (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2 suceloni 7375 . . . . 5 (𝑦 ∈ On → suc 𝑦 ∈ On)
3 fveq2 6530 . . . . . . . 8 (𝑥 = 𝑦 → (𝑅1𝑥) = (𝑅1𝑦))
43raleqdv 3372 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5 fveq2 6530 . . . . . . . . 9 (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6 fveq2 6530 . . . . . . . . . 10 (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
76imaeq2d 5798 . . . . . . . . 9 (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
85, 7sseq12d 3916 . . . . . . . 8 (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
98cbvralv 3400 . . . . . . 7 (∀𝑧 ∈ (𝑅1𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
104, 9syl6bb 288 . . . . . 6 (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11 fveq2 6530 . . . . . . 7 (𝑥 = suc 𝑦 → (𝑅1𝑥) = (𝑅1‘suc 𝑦))
1211raleqdv 3372 . . . . . 6 (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
13 simpr 485 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)))
14 simprl 767 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1𝑥))
15 simplr 765 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
16 rankr1ai 9062 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1𝑥) → (rank‘𝑧) ∈ 𝑥)
17 fveq2 6530 . . . . . . . . . . . . . . . . . 18 (𝑦 = (rank‘𝑧) → (𝑅1𝑦) = (𝑅1‘(rank‘𝑧)))
1817raleqdv 3372 . . . . . . . . . . . . . . . . 17 (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
1918rspcv 3550 . . . . . . . . . . . . . . . 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 9060 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑅1𝑥) → 𝑧 (𝑅1 “ On))
22 r1rankidb 9068 . . . . . . . . . . . . . . . 16 (𝑧 (𝑅1 “ On) → 𝑧 ⊆ (𝑅1‘(rank‘𝑧)))
23 ssralv 3949 . . . . . . . . . . . . . . . 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 9090 . . . . . . . . . . . . . . . . . . . 20 (𝑧 (𝑅1 “ On) → (rank‘𝑧) = {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥})
2827eleq2d 2866 . . . . . . . . . . . . . . . . . . 19 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
2928biimpd 230 . . . . . . . . . . . . . . . . . 18 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 {𝑥 ∈ On ∣ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥}))
30 rankon 9059 . . . . . . . . . . . . . . . . . . . 20 (rank‘𝑧) ∈ On
3130oneli 6165 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32 eleq2w 2864 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
3332ralbidv 3162 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (∀𝑢𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤))
3433onnminsb 7366 . . . . . . . . . . . . . . . . . . 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 407 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤)
39 rexnal 3200 . . . . . . . . . . . . . . 15 (∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢𝑧 (rank‘𝑢) ∈ 𝑤)
4038, 39sylibr 235 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
4140adantl 482 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42 r19.29 3215 . . . . . . . . . . . . 13 ((∀𝑢𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ∃𝑢𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
4326, 41, 42syl2anc 584 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
44 simp2 1128 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢𝑧)
45 tcid 9016 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
4645elv 3437 . . . . . . . . . . . . . . . 16 𝑧 ⊆ (TC‘𝑧)
4746sseli 3880 . . . . . . . . . . . . . . 15 (𝑢𝑧𝑢 ∈ (TC‘𝑧))
48 fveqeq2 6539 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
4948rspcev 3554 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
5049ex 413 . . . . . . . . . . . . . . 15 (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
5144, 47, 503syl 18 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
52 simp3l 1192 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
5352sseld 3883 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢))))
54 simp1l 1188 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1𝑥))
55 rankf 9058 . . . . . . . . . . . . . . . . . . 19 rank: (𝑅1 “ On)⟶On
56 ffn 6374 . . . . . . . . . . . . . . . . . . 19 (rank: (𝑅1 “ On)⟶On → rank Fn (𝑅1 “ On))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . 18 rank Fn (𝑅1 “ On)
58 r1tr 9040 . . . . . . . . . . . . . . . . . . . 20 Tr (𝑅1𝑥)
59 trel 5064 . . . . . . . . . . . . . . . . . . . 20 (Tr (𝑅1𝑥) → ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → 𝑢 ∈ (𝑅1𝑥)))
6058, 59ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → 𝑢 ∈ (𝑅1𝑥))
61 r1elwf 9060 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝑅1𝑥) → 𝑢 (𝑅1 “ On))
62 tcwf 9147 . . . . . . . . . . . . . . . . . . . 20 (𝑢 (𝑅1 “ On) → (TC‘𝑢) ∈ (𝑅1 “ On))
63 fvex 6543 . . . . . . . . . . . . . . . . . . . . 21 (TC‘𝑢) ∈ V
6463r1elss 9070 . . . . . . . . . . . . . . . . . . . 20 ((TC‘𝑢) ∈ (𝑅1 “ On) ↔ (TC‘𝑢) ⊆ (𝑅1 “ On))
6562, 64sylib 219 . . . . . . . . . . . . . . . . . . 19 (𝑢 (𝑅1 “ On) → (TC‘𝑢) ⊆ (𝑅1 “ On))
6660, 61, 653syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (TC‘𝑢) ⊆ (𝑅1 “ On))
67 fvelimab 6597 . . . . . . . . . . . . . . . . . 18 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
6857, 66, 67sylancr 587 . . . . . . . . . . . . . . . . 17 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
69 vex 3435 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
7069tcel 9022 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71 ssrexv 3950 . . . . . . . . . . . . . . . . . . 19 ((TC‘𝑢) ⊆ (TC‘𝑧) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7270, 71syl 17 . . . . . . . . . . . . . . . . . 18 (𝑢𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7372adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7468, 73sylbid 241 . . . . . . . . . . . . . . . 16 ((𝑢𝑧𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
7544, 54, 74syl2anc 584 . . . . . . . . . . . . . . 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 9059 . . . . . . . . . . . . . . . . . . 19 (rank‘𝑢) ∈ On
78 eloni 6068 . . . . . . . . . . . . . . . . . . . 20 ((rank‘𝑢) ∈ On → Ord (rank‘𝑢))
79 eloni 6068 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ On → Ord 𝑤)
80 ordtri3or 6090 . . . . . . . . . . . . . . . . . . . 20 ((Ord (rank‘𝑢) ∧ Ord 𝑤) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8178, 79, 80syl2an 595 . . . . . . . . . . . . . . . . . . 19 (((rank‘𝑢) ∈ On ∧ 𝑤 ∈ On) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8277, 31, 81sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
83 3orass 1081 . . . . . . . . . . . . . . . . . 18 (((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8482, 83sylib 219 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢))))
8584orcanai 995 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8685ad2ant2l 742 . . . . . . . . . . . . . . 15 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
87863adant2 1122 . . . . . . . . . . . . . 14 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤𝑤 ∈ (rank‘𝑢)))
8851, 76, 87mpjaod 855 . . . . . . . . . . . . 13 (((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
8988rexlimdv3a 3246 . . . . . . . . . . . 12 ((𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9013, 43, 89sylc 65 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
9190expr 457 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
92 tcwf 9147 . . . . . . . . . . . . 13 (𝑧 (𝑅1 “ On) → (TC‘𝑧) ∈ (𝑅1 “ On))
93 r1elssi 9069 . . . . . . . . . . . . . 14 ((TC‘𝑧) ∈ (𝑅1 “ On) → (TC‘𝑧) ⊆ (𝑅1 “ On))
94 fvelimab 6597 . . . . . . . . . . . . . 14 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑧) ⊆ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9593, 94sylan2 592 . . . . . . . . . . . . 13 ((rank Fn (𝑅1 “ On) ∧ (TC‘𝑧) ∈ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9657, 92, 95sylancr 587 . . . . . . . . . . . 12 (𝑧 (𝑅1 “ On) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9721, 96syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝑅1𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9897adantl 482 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
9991, 98sylibrd 260 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧))))
10099ssrdv 3890 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101100ralrimiva 3147 . . . . . . 7 ((𝑥 ∈ On ∧ ∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
102101ex 413 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥𝑢 ∈ (𝑅1𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈ (𝑅1𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
10310, 12, 102tfis3 7419 . . . . 5 (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104 fveq2 6530 . . . . . . 7 (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105 fveq2 6530 . . . . . . . 8 (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106105imaeq2d 5798 . . . . . . 7 (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107104, 106sseq12d 3916 . . . . . 6 (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108107rspccv 3551 . . . . 5 (∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
1092, 103, 1083syl 18 . . . 4 (𝑦 ∈ On → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
110109rexlimiv 3240 . . 3 (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
1111, 110sylbi 218 . 2 (𝐴 (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
112 tcvalg 9015 . . . 4 (𝐴 (𝑅1 “ On) → (TC‘𝐴) = {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)})
113 r1rankidb 9068 . . . . 5 (𝐴 (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
114 r1tr 9040 . . . . 5 Tr (𝑅1‘(rank‘𝐴))
115 fvex 6543 . . . . . . 7 (𝑅1‘(rank‘𝐴)) ∈ V
116 sseq2 3909 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (𝐴𝑥𝐴 ⊆ (𝑅1‘(rank‘𝐴))))
117 treq 5063 . . . . . . . 8 (𝑥 = (𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr (𝑅1‘(rank‘𝐴))))
118116, 117anbi12d 630 . . . . . . 7 (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119115, 118elab 3600 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120 intss1 4791 . . . . . 6 ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
121119, 120sylbir 236 . . . . 5 ((𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))) → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
122113, 114, 121sylancl 586 . . . 4 (𝐴 (𝑅1 “ On) → {𝑥 ∣ (𝐴𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
123112, 122eqsstrd 3921 . . 3 (𝐴 (𝑅1 “ On) → (TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)))
124 imass2 5833 . . . 4 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “ (𝑅1‘(rank‘𝐴))))
125 ffun 6377 . . . . . . . 8 (rank: (𝑅1 “ On)⟶On → Fun rank)
12655, 125ax-mp 5 . . . . . . 7 Fun rank
127 fvelima 6591 . . . . . . 7 ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128126, 127mpan 686 . . . . . 6 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129 rankr1ai 9062 . . . . . . . 8 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130 eleq1 2868 . . . . . . . 8 ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131129, 130syl5ibcom 246 . . . . . . 7 (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴)))
132131rexlimiv 3240 . . . . . 6 (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥𝑥 ∈ (rank‘𝐴))
133128, 132syl 17 . . . . 5 (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134133ssriv 3888 . . . 4 (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135124, 134syl6ss 3896 . . 3 ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136123, 135syl 17 . 2 (𝐴 (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137111, 136eqssd 3901 1 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842  w3o 1077  w3a 1078   = wceq 1520  wcel 2079  {cab 2773  wral 3103  wrex 3104  {crab 3107  Vcvv 3432  wss 3854   cuni 4739   cint 4776  Tr wtr 5057  cima 5438  Ord word 6057  Oncon0 6058  suc csuc 6060  Fun wfun 6211   Fn wfn 6212  wf 6213  cfv 6217  TCctc 9013  𝑅1cr1 9026  rankcrnk 9027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-rep 5075  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-inf2 8939
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-int 4777  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-tr 5058  df-id 5340  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-we 5396  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-pred 6015  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-om 7428  df-wrecs 7789  df-recs 7851  df-rdg 7889  df-tc 9014  df-r1 9028  df-rank 9029
This theorem is referenced by:  hsmexlem5  9687  grur1  10077
  Copyright terms: Public domain W3C validator