Metamath Proof Explorer


Theorem tcrank

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 A . Stated another way, to construct a set at a given rank, you have to climb the entire hierarchy of ordinals below ( rankA ) , 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 ( TCA ) has a rank below the rank of A , since intuitively it contains only the members of A and the members of those and so on, but nothing "bigger" than A . (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tcrank ( 𝐴 ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ( rank “ ( TC ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 rankwflemb ( 𝐴 ( 𝑅1 “ On ) ↔ ∃ 𝑦 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑦 ) )
2 suceloni ( 𝑦 ∈ On → suc 𝑦 ∈ On )
3 fveq2 ( 𝑥 = 𝑦 → ( 𝑅1𝑥 ) = ( 𝑅1𝑦 ) )
4 3 raleqdv ( 𝑥 = 𝑦 → ( ∀ 𝑧 ∈ ( 𝑅1𝑥 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ) )
5 fveq2 ( 𝑧 = 𝑢 → ( rank ‘ 𝑧 ) = ( rank ‘ 𝑢 ) )
6 fveq2 ( 𝑧 = 𝑢 → ( TC ‘ 𝑧 ) = ( TC ‘ 𝑢 ) )
7 6 imaeq2d ( 𝑧 = 𝑢 → ( rank “ ( TC ‘ 𝑧 ) ) = ( rank “ ( TC ‘ 𝑢 ) ) )
8 5 7 sseq12d ( 𝑧 = 𝑢 → ( ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
9 8 cbvralvw ( ∀ 𝑧 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∀ 𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) )
10 4 9 bitrdi ( 𝑥 = 𝑦 → ( ∀ 𝑧 ∈ ( 𝑅1𝑥 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∀ 𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
11 fveq2 ( 𝑥 = suc 𝑦 → ( 𝑅1𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
12 11 raleqdv ( 𝑥 = suc 𝑦 → ( ∀ 𝑧 ∈ ( 𝑅1𝑥 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝑅1 ‘ suc 𝑦 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ) )
13 simpr ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ) → ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) )
14 simprl ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ) → 𝑧 ∈ ( 𝑅1𝑥 ) )
15 simplr ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ) → ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) )
16 rankr1ai ( 𝑧 ∈ ( 𝑅1𝑥 ) → ( rank ‘ 𝑧 ) ∈ 𝑥 )
17 fveq2 ( 𝑦 = ( rank ‘ 𝑧 ) → ( 𝑅1𝑦 ) = ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) )
18 17 raleqdv ( 𝑦 = ( rank ‘ 𝑧 ) → ( ∀ 𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
19 18 rspcv ( ( rank ‘ 𝑧 ) ∈ 𝑥 → ( ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) → ∀ 𝑢 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
20 16 19 syl ( 𝑧 ∈ ( 𝑅1𝑥 ) → ( ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) → ∀ 𝑢 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
21 r1elwf ( 𝑧 ∈ ( 𝑅1𝑥 ) → 𝑧 ( 𝑅1 “ On ) )
22 r1rankidb ( 𝑧 ( 𝑅1 “ On ) → 𝑧 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) )
23 ssralv ( 𝑧 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) → ( ∀ 𝑢 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) → ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
24 21 22 23 3syl ( 𝑧 ∈ ( 𝑅1𝑥 ) → ( ∀ 𝑢 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑧 ) ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) → ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
25 20 24 syld ( 𝑧 ∈ ( 𝑅1𝑥 ) → ( ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) → ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) )
26 14 15 25 sylc ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ) → ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) )
27 rankval3b ( 𝑧 ( 𝑅1 “ On ) → ( rank ‘ 𝑧 ) = { 𝑥 ∈ On ∣ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑥 } )
28 27 eleq2d ( 𝑧 ( 𝑅1 “ On ) → ( 𝑤 ∈ ( rank ‘ 𝑧 ) ↔ 𝑤 { 𝑥 ∈ On ∣ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑥 } ) )
29 28 biimpd ( 𝑧 ( 𝑅1 “ On ) → ( 𝑤 ∈ ( rank ‘ 𝑧 ) → 𝑤 { 𝑥 ∈ On ∣ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑥 } ) )
30 rankon ( rank ‘ 𝑧 ) ∈ On
31 30 oneli ( 𝑤 ∈ ( rank ‘ 𝑧 ) → 𝑤 ∈ On )
32 eleq2w ( 𝑥 = 𝑤 → ( ( rank ‘ 𝑢 ) ∈ 𝑥 ↔ ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
33 32 ralbidv ( 𝑥 = 𝑤 → ( ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑥 ↔ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
34 33 onnminsb ( 𝑤 ∈ On → ( 𝑤 { 𝑥 ∈ On ∣ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑥 } → ¬ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
35 31 34 syl ( 𝑤 ∈ ( rank ‘ 𝑧 ) → ( 𝑤 { 𝑥 ∈ On ∣ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑥 } → ¬ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
36 29 35 sylcom ( 𝑧 ( 𝑅1 “ On ) → ( 𝑤 ∈ ( rank ‘ 𝑧 ) → ¬ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
37 21 36 syl ( 𝑧 ∈ ( 𝑅1𝑥 ) → ( 𝑤 ∈ ( rank ‘ 𝑧 ) → ¬ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
38 37 imp ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) → ¬ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑤 )
39 rexnal ( ∃ 𝑢𝑧 ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ↔ ¬ ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ∈ 𝑤 )
40 38 39 sylibr ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) → ∃ 𝑢𝑧 ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 )
41 40 adantl ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ) → ∃ 𝑢𝑧 ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 )
42 r19.29 ( ( ∀ 𝑢𝑧 ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ∃ 𝑢𝑧 ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) → ∃ 𝑢𝑧 ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
43 26 41 42 syl2anc ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ) → ∃ 𝑢𝑧 ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) )
44 simp2 ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → 𝑢𝑧 )
45 tcid ( 𝑧 ∈ V → 𝑧 ⊆ ( TC ‘ 𝑧 ) )
46 45 elv 𝑧 ⊆ ( TC ‘ 𝑧 )
47 46 sseli ( 𝑢𝑧𝑢 ∈ ( TC ‘ 𝑧 ) )
48 fveqeq2 ( 𝑥 = 𝑢 → ( ( rank ‘ 𝑥 ) = 𝑤 ↔ ( rank ‘ 𝑢 ) = 𝑤 ) )
49 48 rspcev ( ( 𝑢 ∈ ( TC ‘ 𝑧 ) ∧ ( rank ‘ 𝑢 ) = 𝑤 ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 )
50 49 ex ( 𝑢 ∈ ( TC ‘ 𝑧 ) → ( ( rank ‘ 𝑢 ) = 𝑤 → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
51 44 47 50 3syl ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ( ( rank ‘ 𝑢 ) = 𝑤 → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
52 simp3l ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) )
53 52 sseld ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ( 𝑤 ∈ ( rank ‘ 𝑢 ) → 𝑤 ∈ ( rank “ ( TC ‘ 𝑢 ) ) ) )
54 simp1l ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → 𝑧 ∈ ( 𝑅1𝑥 ) )
55 rankf rank : ( 𝑅1 “ On ) ⟶ On
56 ffn ( rank : ( 𝑅1 “ On ) ⟶ On → rank Fn ( 𝑅1 “ On ) )
57 55 56 ax-mp rank Fn ( 𝑅1 “ On )
58 r1tr Tr ( 𝑅1𝑥 )
59 trel ( Tr ( 𝑅1𝑥 ) → ( ( 𝑢𝑧𝑧 ∈ ( 𝑅1𝑥 ) ) → 𝑢 ∈ ( 𝑅1𝑥 ) ) )
60 58 59 ax-mp ( ( 𝑢𝑧𝑧 ∈ ( 𝑅1𝑥 ) ) → 𝑢 ∈ ( 𝑅1𝑥 ) )
61 r1elwf ( 𝑢 ∈ ( 𝑅1𝑥 ) → 𝑢 ( 𝑅1 “ On ) )
62 tcwf ( 𝑢 ( 𝑅1 “ On ) → ( TC ‘ 𝑢 ) ∈ ( 𝑅1 “ On ) )
63 fvex ( TC ‘ 𝑢 ) ∈ V
64 63 r1elss ( ( TC ‘ 𝑢 ) ∈ ( 𝑅1 “ On ) ↔ ( TC ‘ 𝑢 ) ⊆ ( 𝑅1 “ On ) )
65 62 64 sylib ( 𝑢 ( 𝑅1 “ On ) → ( TC ‘ 𝑢 ) ⊆ ( 𝑅1 “ On ) )
66 60 61 65 3syl ( ( 𝑢𝑧𝑧 ∈ ( 𝑅1𝑥 ) ) → ( TC ‘ 𝑢 ) ⊆ ( 𝑅1 “ On ) )
67 fvelimab ( ( rank Fn ( 𝑅1 “ On ) ∧ ( TC ‘ 𝑢 ) ⊆ ( 𝑅1 “ On ) ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑢 ) ) ↔ ∃ 𝑥 ∈ ( TC ‘ 𝑢 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
68 57 66 67 sylancr ( ( 𝑢𝑧𝑧 ∈ ( 𝑅1𝑥 ) ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑢 ) ) ↔ ∃ 𝑥 ∈ ( TC ‘ 𝑢 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
69 vex 𝑧 ∈ V
70 69 tcel ( 𝑢𝑧 → ( TC ‘ 𝑢 ) ⊆ ( TC ‘ 𝑧 ) )
71 ssrexv ( ( TC ‘ 𝑢 ) ⊆ ( TC ‘ 𝑧 ) → ( ∃ 𝑥 ∈ ( TC ‘ 𝑢 ) ( rank ‘ 𝑥 ) = 𝑤 → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
72 70 71 syl ( 𝑢𝑧 → ( ∃ 𝑥 ∈ ( TC ‘ 𝑢 ) ( rank ‘ 𝑥 ) = 𝑤 → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
73 72 adantr ( ( 𝑢𝑧𝑧 ∈ ( 𝑅1𝑥 ) ) → ( ∃ 𝑥 ∈ ( TC ‘ 𝑢 ) ( rank ‘ 𝑥 ) = 𝑤 → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
74 68 73 sylbid ( ( 𝑢𝑧𝑧 ∈ ( 𝑅1𝑥 ) ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑢 ) ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
75 44 54 74 syl2anc ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑢 ) ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
76 53 75 syld ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ( 𝑤 ∈ ( rank ‘ 𝑢 ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
77 rankon ( rank ‘ 𝑢 ) ∈ On
78 eloni ( ( rank ‘ 𝑢 ) ∈ On → Ord ( rank ‘ 𝑢 ) )
79 eloni ( 𝑤 ∈ On → Ord 𝑤 )
80 ordtri3or ( ( Ord ( rank ‘ 𝑢 ) ∧ Ord 𝑤 ) → ( ( rank ‘ 𝑢 ) ∈ 𝑤 ∨ ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) )
81 78 79 80 syl2an ( ( ( rank ‘ 𝑢 ) ∈ On ∧ 𝑤 ∈ On ) → ( ( rank ‘ 𝑢 ) ∈ 𝑤 ∨ ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) )
82 77 31 81 sylancr ( 𝑤 ∈ ( rank ‘ 𝑧 ) → ( ( rank ‘ 𝑢 ) ∈ 𝑤 ∨ ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) )
83 3orass ( ( ( rank ‘ 𝑢 ) ∈ 𝑤 ∨ ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) ↔ ( ( rank ‘ 𝑢 ) ∈ 𝑤 ∨ ( ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) ) )
84 82 83 sylib ( 𝑤 ∈ ( rank ‘ 𝑧 ) → ( ( rank ‘ 𝑢 ) ∈ 𝑤 ∨ ( ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) ) )
85 84 orcanai ( ( 𝑤 ∈ ( rank ‘ 𝑧 ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) → ( ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) )
86 85 ad2ant2l ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ( ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) )
87 86 3adant2 ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ( ( rank ‘ 𝑢 ) = 𝑤𝑤 ∈ ( rank ‘ 𝑢 ) ) )
88 51 76 87 mpjaod ( ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ∧ 𝑢𝑧 ∧ ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 )
89 88 rexlimdv3a ( ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) → ( ∃ 𝑢𝑧 ( ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ∧ ¬ ( rank ‘ 𝑢 ) ∈ 𝑤 ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
90 13 43 89 sylc ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑅1𝑥 ) ∧ 𝑤 ∈ ( rank ‘ 𝑧 ) ) ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 )
91 90 expr ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ 𝑧 ∈ ( 𝑅1𝑥 ) ) → ( 𝑤 ∈ ( rank ‘ 𝑧 ) → ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
92 tcwf ( 𝑧 ( 𝑅1 “ On ) → ( TC ‘ 𝑧 ) ∈ ( 𝑅1 “ On ) )
93 r1elssi ( ( TC ‘ 𝑧 ) ∈ ( 𝑅1 “ On ) → ( TC ‘ 𝑧 ) ⊆ ( 𝑅1 “ On ) )
94 fvelimab ( ( rank Fn ( 𝑅1 “ On ) ∧ ( TC ‘ 𝑧 ) ⊆ ( 𝑅1 “ On ) ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
95 93 94 sylan2 ( ( rank Fn ( 𝑅1 “ On ) ∧ ( TC ‘ 𝑧 ) ∈ ( 𝑅1 “ On ) ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
96 57 92 95 sylancr ( 𝑧 ( 𝑅1 “ On ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
97 21 96 syl ( 𝑧 ∈ ( 𝑅1𝑥 ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
98 97 adantl ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ 𝑧 ∈ ( 𝑅1𝑥 ) ) → ( 𝑤 ∈ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ( TC ‘ 𝑧 ) ( rank ‘ 𝑥 ) = 𝑤 ) )
99 91 98 sylibrd ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ 𝑧 ∈ ( 𝑅1𝑥 ) ) → ( 𝑤 ∈ ( rank ‘ 𝑧 ) → 𝑤 ∈ ( rank “ ( TC ‘ 𝑧 ) ) ) )
100 99 ssrdv ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) ∧ 𝑧 ∈ ( 𝑅1𝑥 ) ) → ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) )
101 100 ralrimiva ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) ) → ∀ 𝑧 ∈ ( 𝑅1𝑥 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) )
102 101 ex ( 𝑥 ∈ On → ( ∀ 𝑦𝑥𝑢 ∈ ( 𝑅1𝑦 ) ( rank ‘ 𝑢 ) ⊆ ( rank “ ( TC ‘ 𝑢 ) ) → ∀ 𝑧 ∈ ( 𝑅1𝑥 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ) )
103 10 12 102 tfis3 ( suc 𝑦 ∈ On → ∀ 𝑧 ∈ ( 𝑅1 ‘ suc 𝑦 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) )
104 fveq2 ( 𝑧 = 𝐴 → ( rank ‘ 𝑧 ) = ( rank ‘ 𝐴 ) )
105 fveq2 ( 𝑧 = 𝐴 → ( TC ‘ 𝑧 ) = ( TC ‘ 𝐴 ) )
106 105 imaeq2d ( 𝑧 = 𝐴 → ( rank “ ( TC ‘ 𝑧 ) ) = ( rank “ ( TC ‘ 𝐴 ) ) )
107 104 106 sseq12d ( 𝑧 = 𝐴 → ( ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) ↔ ( rank ‘ 𝐴 ) ⊆ ( rank “ ( TC ‘ 𝐴 ) ) ) )
108 107 rspccv ( ∀ 𝑧 ∈ ( 𝑅1 ‘ suc 𝑦 ) ( rank ‘ 𝑧 ) ⊆ ( rank “ ( TC ‘ 𝑧 ) ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑦 ) → ( rank ‘ 𝐴 ) ⊆ ( rank “ ( TC ‘ 𝐴 ) ) ) )
109 2 103 108 3syl ( 𝑦 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑦 ) → ( rank ‘ 𝐴 ) ⊆ ( rank “ ( TC ‘ 𝐴 ) ) ) )
110 109 rexlimiv ( ∃ 𝑦 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑦 ) → ( rank ‘ 𝐴 ) ⊆ ( rank “ ( TC ‘ 𝐴 ) ) )
111 1 110 sylbi ( 𝐴 ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ( rank “ ( TC ‘ 𝐴 ) ) )
112 tcvalg ( 𝐴 ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) = { 𝑥 ∣ ( 𝐴𝑥 ∧ Tr 𝑥 ) } )
113 r1rankidb ( 𝐴 ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
114 r1tr Tr ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
115 fvex ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ V
116 sseq2 ( 𝑥 = ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( 𝐴𝑥𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
117 treq ( 𝑥 = ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( Tr 𝑥 ↔ Tr ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
118 116 117 anbi12d ( 𝑥 = ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( ( 𝐴𝑥 ∧ Tr 𝑥 ) ↔ ( 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∧ Tr ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) ) )
119 115 118 elab ( ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ { 𝑥 ∣ ( 𝐴𝑥 ∧ Tr 𝑥 ) } ↔ ( 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∧ Tr ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
120 intss1 ( ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ { 𝑥 ∣ ( 𝐴𝑥 ∧ Tr 𝑥 ) } → { 𝑥 ∣ ( 𝐴𝑥 ∧ Tr 𝑥 ) } ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
121 119 120 sylbir ( ( 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∧ Tr ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) → { 𝑥 ∣ ( 𝐴𝑥 ∧ Tr 𝑥 ) } ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
122 113 114 121 sylancl ( 𝐴 ( 𝑅1 “ On ) → { 𝑥 ∣ ( 𝐴𝑥 ∧ Tr 𝑥 ) } ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
123 112 122 eqsstrd ( 𝐴 ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
124 imass2 ( ( TC ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( rank “ ( TC ‘ 𝐴 ) ) ⊆ ( rank “ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
125 ffun ( rank : ( 𝑅1 “ On ) ⟶ On → Fun rank )
126 55 125 ax-mp Fun rank
127 fvelima ( ( Fun rank ∧ 𝑥 ∈ ( rank “ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) ) → ∃ 𝑦 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ( rank ‘ 𝑦 ) = 𝑥 )
128 126 127 mpan ( 𝑥 ∈ ( rank “ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ( rank ‘ 𝑦 ) = 𝑥 )
129 rankr1ai ( 𝑦 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) )
130 eleq1 ( ( rank ‘ 𝑦 ) = 𝑥 → ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) ↔ 𝑥 ∈ ( rank ‘ 𝐴 ) ) )
131 129 130 syl5ibcom ( 𝑦 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( ( rank ‘ 𝑦 ) = 𝑥𝑥 ∈ ( rank ‘ 𝐴 ) ) )
132 131 rexlimiv ( ∃ 𝑦 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ( rank ‘ 𝑦 ) = 𝑥𝑥 ∈ ( rank ‘ 𝐴 ) )
133 128 132 syl ( 𝑥 ∈ ( rank “ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) → 𝑥 ∈ ( rank ‘ 𝐴 ) )
134 133 ssriv ( rank “ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) ⊆ ( rank ‘ 𝐴 )
135 124 134 sstrdi ( ( TC ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( rank “ ( TC ‘ 𝐴 ) ) ⊆ ( rank ‘ 𝐴 ) )
136 123 135 syl ( 𝐴 ( 𝑅1 “ On ) → ( rank “ ( TC ‘ 𝐴 ) ) ⊆ ( rank ‘ 𝐴 ) )
137 111 136 eqssd ( 𝐴 ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ( rank “ ( TC ‘ 𝐴 ) ) )