Theorem tcrank 9837

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.

Step	Hyp	Ref	Expression
1		rankwflemb 9746	. . 3 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2		onsuc 7787	. . . . 5 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
3		fveq2 6858	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
4	3	raleqdv 3299	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5		fveq2 6858	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
7	6	imaeq2d 6031	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
8	5, 7	sseq12d 3980	. . . . . . . 8 ⊢ (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
9	8	cbvralvw 3215	. . . . . . 7 ⊢ (∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
10	4, 9	bitrdi 287	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11		fveq2 6858	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
12	11	raleqdv 3299	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
13		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)))
14		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1‘𝑥))
15		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
16		rankr1ai 9751	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥)
17		fveq2 6858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (rank‘𝑧) → (𝑅1‘𝑦) = (𝑅1‘(rank‘𝑧)))
18	17	raleqdv 3299	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
19	18	rspcv 3584	. . . . . . . . . . . . . . . 16 ⊢ ((rank‘𝑧) ∈ 𝑥 → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
20	16, 19	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
21		r1elwf 9749	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → 𝑧 ∈ ∪ (𝑅1 “ On))
22		r1rankidb 9757	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆ (𝑅1‘(rank‘𝑧)))
23		ssralv 4015	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ (𝑅1‘(rank‘𝑧)) → (∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
24	21, 22, 23	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
25	20, 24	syld 47	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
26	14, 15, 25	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
27		rankval3b 9779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (rank‘𝑧) = ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})
28	27	eleq2d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
29	28	biimpd 229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
30		rankon 9748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (rank‘𝑧) ∈ On
31	30	oneli 6448	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32		eleq2w 2812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
33	32	ralbidv 3156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
34	33	onnminsb 7775	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ On → (𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
35	31, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (rank‘𝑧) → (𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥} → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
36	29, 35	sylcom 30	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
37	21, 36	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (𝑤 ∈ (rank‘𝑧) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
38	37	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)
39		rexnal 3082	. . . . . . . . . . . . . . 15 ⊢ (∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)
40	38, 39	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
41	40	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42		r19.29 3094	. . . . . . . . . . . . 13 ⊢ ((∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
43	26, 41, 42	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
44		simp2 1137	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢 ∈ 𝑧)
45		tcid 9692	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
46	45	elv 3452	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ⊆ (TC‘𝑧)
47	46	sseli 3942	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧))
48		fveqeq2 6867	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
49	48	rspcev 3588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
50	49	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
51	44, 47, 50	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
52		simp3l 1202	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
53	52	sseld 3945	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢))))
54		simp1l 1198	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥))
55		rankf 9747	. . . . . . . . . . . . . . . . . . 19 ⊢ rank:∪ (𝑅1 “ On)⟶On
56		ffn 6688	. . . . . . . . . . . . . . . . . . 19 ⊢ (rank:∪ (𝑅1 “ On)⟶On → rank Fn ∪ (𝑅1 “ On))
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ rank Fn ∪ (𝑅1 “ On)
58		r1tr 9729	. . . . . . . . . . . . . . . . . . . 20 ⊢ Tr (𝑅1‘𝑥)
59		trel 5223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr (𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)))
60	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))
61		r1elwf 9749	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝑅1‘𝑥) → 𝑢 ∈ ∪ (𝑅1 “ On))
62		tcwf 9836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ ∪ (𝑅1 “ On) → (TC‘𝑢) ∈ ∪ (𝑅1 “ On))
63		fvex 6871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TC‘𝑢) ∈ V
64	63	r1elss 9759	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((TC‘𝑢) ∈ ∪ (𝑅1 “ On) ↔ (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
65	62, 64	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ ∪ (𝑅1 “ On) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
66	60, 61, 65	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
67		fvelimab 6933	. . . . . . . . . . . . . . . . . 18 ⊢ ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
68	57, 66, 67	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
69		vex 3451	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
70	69	tcel 9698	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71		ssrexv 4016	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TC‘𝑢) ⊆ (TC‘𝑧) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
72	70, 71	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
73	72	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
74	68, 73	sylbid 240	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
75	44, 54, 74	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
76	53, 75	syld 47	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
77		rankon 9748	. . . . . . . . . . . . . . . . . . 19 ⊢ (rank‘𝑢) ∈ On
78		eloni 6342	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((rank‘𝑢) ∈ On → Ord (rank‘𝑢))
79		eloni 6342	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ On → Ord 𝑤)
80		ordtri3or 6364	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord (rank‘𝑢) ∧ Ord 𝑤) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
81	78, 79, 80	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((rank‘𝑢) ∈ On ∧ 𝑤 ∈ On) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
82	77, 31, 81	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
83		3orass 1089	. . . . . . . . . . . . . . . . . 18 ⊢ (((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))))
84	82, 83	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))))
85	84	orcanai 1004	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
86	85	ad2ant2l 746	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
87	86	3adant2 1131	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
88	51, 76, 87	mpjaod 860	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
89	88	rexlimdv3a 3138	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → (∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
90	13, 43, 89	sylc 65	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
91	90	expr 456	. . . . . . . . . 10 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
92		tcwf 9836	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ∈ ∪ (𝑅1 “ On))
93		r1elssi 9758	. . . . . . . . . . . . . 14 ⊢ ((TC‘𝑧) ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ⊆ ∪ (𝑅1 “ On))
94		fvelimab 6933	. . . . . . . . . . . . . 14 ⊢ ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
95	93, 94	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑧) ∈ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
96	57, 92, 95	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
97	21, 96	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
98	97	adantl 481	. . . . . . . . . 10 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
99	91, 98	sylibrd 259	. . . . . . . . 9 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧))))
100	99	ssrdv 3952	. . . . . . . 8 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101	100	ralrimiva 3125	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
102	101	ex 412	. . . . . 6 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
103	10, 12, 102	tfis3 7834	. . . . 5 ⊢ (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104		fveq2 6858	. . . . . . 7 ⊢ (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105		fveq2 6858	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106	105	imaeq2d 6031	. . . . . . 7 ⊢ (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107	104, 106	sseq12d 3980	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108	107	rspccv 3585	. . . . 5 ⊢ (∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
109	2, 103, 108	3syl 18	. . . 4 ⊢ (𝑦 ∈ On → (𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
110	109	rexlimiv 3127	. . 3 ⊢ (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
111	1, 110	sylbi 217	. 2 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
112		tcvalg 9691	. . . 4 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)})
113		r1rankidb 9757	. . . . 5 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
114		r1tr 9729	. . . . 5 ⊢ Tr (𝑅1‘(rank‘𝐴))
115		fvex 6871	. . . . . . 7 ⊢ (𝑅1‘(rank‘𝐴)) ∈ V
116		sseq2 3973	. . . . . . . 8 ⊢ (𝑥 = (𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (𝑅1‘(rank‘𝐴))))
117		treq 5222	. . . . . . . 8 ⊢ (𝑥 = (𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr (𝑅1‘(rank‘𝐴))))
118	116, 117	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119	115, 118	elab 3646	. . . . . 6 ⊢ ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120		intss1 4927	. . . . . 6 ⊢ ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
121	119, 120	sylbir 235	. . . . 5 ⊢ ((𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))) → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
122	113, 114, 121	sylancl 586	. . . 4 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
123	112, 122	eqsstrd 3981	. . 3 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)))
124		imass2 6073	. . . 4 ⊢ ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “ (𝑅1‘(rank‘𝐴))))
125		ffun 6691	. . . . . . . 8 ⊢ (rank:∪ (𝑅1 “ On)⟶On → Fun rank)
126	55, 125	ax-mp 5	. . . . . . 7 ⊢ Fun rank
127		fvelima 6926	. . . . . . 7 ⊢ ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128	126, 127	mpan 690	. . . . . 6 ⊢ (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129		rankr1ai 9751	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130		eleq1 2816	. . . . . . . 8 ⊢ ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131	129, 130	syl5ibcom 245	. . . . . . 7 ⊢ (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)))
132	131	rexlimiv 3127	. . . . . 6 ⊢ (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))
133	128, 132	syl 17	. . . . 5 ⊢ (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134	133	ssriv 3950	. . . 4 ⊢ (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135	124, 134	sstrdi 3959	. . 3 ⊢ ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136	123, 135	syl 17	. 2 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137	111, 136	eqssd 3964	1 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053  {crab 3405  Vcvv 3447   ⊆ wss 3914  ∪ cuni 4871  ∩ cint 4910  Tr wtr 5214   “ cima 5641  Ord word 6331  Oncon0 6332  suc csuc 6334  Fun wfun 6505   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  TCctc 9689  𝑅₁cr1 9715  rankcrnk 9716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-tc 9690  df-r1 9717  df-rank 9718

This theorem is referenced by:  hsmexlem5  10383  grur1  10773