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 onsuc ⊢ ( 𝑦 ∈ 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 ‘ 𝐴 ) ) )