Theorem tcrank 9800

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 9709	. . 3 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦))
2		onsuc 7754	. . . . 5 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
3		fveq2 6828	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
4	3	raleqdv 3297	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
5		fveq2 6828	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (rank‘𝑧) = (rank‘𝑢))
6		fveq2 6828	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (TC‘𝑧) = (TC‘𝑢))
7	6	imaeq2d 6013	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝑢)))
8	5, 7	sseq12d 3948	. . . . . . . 8 ⊢ (𝑧 = 𝑢 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
9	8	cbvralvw 3217	. . . . . . 7 ⊢ (∀𝑧 ∈ (𝑅1‘𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
10	4, 9	bitrdi 288	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
11		fveq2 6828	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
12	11	raleqdv 3297	. . . . . 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 776	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → 𝑧 ∈ (𝑅1‘𝑥))
15		simplr 774	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
16		rankr1ai 9714	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (rank‘𝑧) ∈ 𝑥)
17		fveq2 6828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (rank‘𝑧) → (𝑅1‘𝑦) = (𝑅1‘(rank‘𝑧)))
18	17	raleqdv 3297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (rank‘𝑧) → (∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ↔ ∀𝑢 ∈ (𝑅1‘(rank‘𝑧))(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))))
19	18	rspcv 3556	. . . . . . . . . . . . . . . 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 9712	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → 𝑧 ∈ ∪ (𝑅1 “ On))
22		r1rankidb 9720	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ⊆ (𝑅1‘(rank‘𝑧)))
23		ssralv 3984	. . . . . . . . . . . . . . . 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 9742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (rank‘𝑧) = ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥})
28	27	eleq2d 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) ↔ 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
29	28	biimpd 230	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ ∩ {𝑥 ∈ On ∣ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥}))
30		rankon 9711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (rank‘𝑧) ∈ On
31	30	oneli 6426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ On)
32		eleq2w 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑤 → ((rank‘𝑢) ∈ 𝑥 ↔ (rank‘𝑢) ∈ 𝑤))
33	32	ralbidv 3162	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑥 ↔ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤))
34	33	onnminsb 7743	. . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)
39		rexnal 3091	. . . . . . . . . . . . . . 15 ⊢ (∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤 ↔ ¬ ∀𝑢 ∈ 𝑧 (rank‘𝑢) ∈ 𝑤)
40	38, 39	sylibr 235	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
41	40	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤)
42		r19.29 3102	. . . . . . . . . . . . 13 ⊢ ((∀𝑢 ∈ 𝑧 (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ∃𝑢 ∈ 𝑧 ¬ (rank‘𝑢) ∈ 𝑤) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
43	26, 41, 42	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ (𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧))) → ∃𝑢 ∈ 𝑧 ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤))
44		simp2 1143	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑢 ∈ 𝑧)
45		tcid 9650	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → 𝑧 ⊆ (TC‘𝑧))
46	45	elv 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ⊆ (TC‘𝑧)
47	46	sseli 3911	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ 𝑧 → 𝑢 ∈ (TC‘𝑧))
48		fveqeq2 6837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → ((rank‘𝑥) = 𝑤 ↔ (rank‘𝑢) = 𝑤))
49	48	rspcev 3560	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (TC‘𝑧) ∧ (rank‘𝑢) = 𝑤) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
50	49	ex 413	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (TC‘𝑧) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
51	44, 47, 50	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
52		simp3l 1208	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (rank‘𝑢) ⊆ (rank “ (TC‘𝑢)))
53	52	sseld 3914	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → (𝑤 ∈ (rank‘𝑢) → 𝑤 ∈ (rank “ (TC‘𝑢))))
54		simp1l 1204	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → 𝑧 ∈ (𝑅1‘𝑥))
55		rankf 9710	. . . . . . . . . . . . . . . . . . 19 ⊢ rank:∪ (𝑅1 “ On)⟶On
56		ffn 6656	. . . . . . . . . . . . . . . . . . 19 ⊢ (rank:∪ (𝑅1 “ On)⟶On → rank Fn ∪ (𝑅1 “ On))
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ rank Fn ∪ (𝑅1 “ On)
58		r1tr 9692	. . . . . . . . . . . . . . . . . . . 20 ⊢ Tr (𝑅1‘𝑥)
59		trel 5188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr (𝑅1‘𝑥) → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥)))
60	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → 𝑢 ∈ (𝑅1‘𝑥))
61		r1elwf 9712	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝑅1‘𝑥) → 𝑢 ∈ ∪ (𝑅1 “ On))
62		tcwf 9799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ ∪ (𝑅1 “ On) → (TC‘𝑢) ∈ ∪ (𝑅1 “ On))
63		fvex 6841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TC‘𝑢) ∈ V
64	63	r1elss 9722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((TC‘𝑢) ∈ ∪ (𝑅1 “ On) ↔ (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
65	62, 64	sylib 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ ∪ (𝑅1 “ On) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
66	60, 61, 65	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (TC‘𝑢) ⊆ ∪ (𝑅1 “ On))
67		fvelimab 6900	. . . . . . . . . . . . . . . . . 18 ⊢ ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑢) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
68	57, 66, 67	sylancr 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) ↔ ∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤))
69		vex 3435	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
70	69	tcel 9656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝑧 → (TC‘𝑢) ⊆ (TC‘𝑧))
71		ssrexv 3985	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TC‘𝑢) ⊆ (TC‘𝑧) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
72	70, 71	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝑧 → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
73	72	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (∃𝑥 ∈ (TC‘𝑢)(rank‘𝑥) = 𝑤 → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
74	68, 73	sylbid 241	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑢)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
75	44, 54, 74	syl2anc 590	. . . . . . . . . . . . . . 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 9711	. . . . . . . . . . . . . . . . . . 19 ⊢ (rank‘𝑢) ∈ On
78		eloni 6321	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((rank‘𝑢) ∈ On → Ord (rank‘𝑢))
79		eloni 6321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ On → Ord 𝑤)
80		ordtri3or 6343	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord (rank‘𝑢) ∧ Ord 𝑤) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
81	78, 79, 80	syl2an 602	. . . . . . . . . . . . . . . . . . 19 ⊢ (((rank‘𝑢) ∈ On ∧ 𝑤 ∈ On) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
82	77, 31, 81	sylancr 593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
83		3orass 1095	. . . . . . . . . . . . . . . . . 18 ⊢ (((rank‘𝑢) ∈ 𝑤 ∨ (rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)) ↔ ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))))
84	82, 83	sylib 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (rank‘𝑧) → ((rank‘𝑢) ∈ 𝑤 ∨ ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢))))
85	84	orcanai 1010	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (rank‘𝑧) ∧ ¬ (rank‘𝑢) ∈ 𝑤) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
86	85	ad2ant2l 752	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
87	86	3adant2 1137	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ((rank‘𝑢) = 𝑤 ∨ 𝑤 ∈ (rank‘𝑢)))
88	51, 76, 87	mpjaod 866	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝑅1‘𝑥) ∧ 𝑤 ∈ (rank‘𝑧)) ∧ 𝑢 ∈ 𝑧 ∧ ((rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) ∧ ¬ (rank‘𝑢) ∈ 𝑤)) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤)
89	88	rexlimdv3a 3144	. . . . . . . . . . . 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 457	. . . . . . . . . 10 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
92		tcwf 9799	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ∈ ∪ (𝑅1 “ On))
93		r1elssi 9721	. . . . . . . . . . . . . 14 ⊢ ((TC‘𝑧) ∈ ∪ (𝑅1 “ On) → (TC‘𝑧) ⊆ ∪ (𝑅1 “ On))
94		fvelimab 6900	. . . . . . . . . . . . . 14 ⊢ ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑧) ⊆ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
95	93, 94	sylan2 599	. . . . . . . . . . . . 13 ⊢ ((rank Fn ∪ (𝑅1 “ On) ∧ (TC‘𝑧) ∈ ∪ (𝑅1 “ On)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
96	57, 92, 95	sylancr 593	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
97	21, 96	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑅1‘𝑥) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
98	97	adantl 482	. . . . . . . . . 10 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank “ (TC‘𝑧)) ↔ ∃𝑥 ∈ (TC‘𝑧)(rank‘𝑥) = 𝑤))
99	91, 98	sylibrd 260	. . . . . . . . 9 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (𝑤 ∈ (rank‘𝑧) → 𝑤 ∈ (rank “ (TC‘𝑧))))
100	99	ssrdv 3921	. . . . . . . 8 ⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) ∧ 𝑧 ∈ (𝑅1‘𝑥)) → (rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
101	100	ralrimiva 3131	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢))) → ∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
102	101	ex 413	. . . . . 6 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ∀𝑢 ∈ (𝑅1‘𝑦)(rank‘𝑢) ⊆ (rank “ (TC‘𝑢)) → ∀𝑧 ∈ (𝑅1‘𝑥)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧))))
103	10, 12, 102	tfis3 7799	. . . . 5 ⊢ (suc 𝑦 ∈ On → ∀𝑧 ∈ (𝑅1‘suc 𝑦)(rank‘𝑧) ⊆ (rank “ (TC‘𝑧)))
104		fveq2 6828	. . . . . . 7 ⊢ (𝑧 = 𝐴 → (rank‘𝑧) = (rank‘𝐴))
105		fveq2 6828	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (TC‘𝑧) = (TC‘𝐴))
106	105	imaeq2d 6013	. . . . . . 7 ⊢ (𝑧 = 𝐴 → (rank “ (TC‘𝑧)) = (rank “ (TC‘𝐴)))
107	104, 106	sseq12d 3948	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((rank‘𝑧) ⊆ (rank “ (TC‘𝑧)) ↔ (rank‘𝐴) ⊆ (rank “ (TC‘𝐴))))
108	107	rspccv 3557	. . . . 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 3133	. . 3 ⊢ (∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑦) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
111	1, 110	sylbi 218	. 2 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank “ (TC‘𝐴)))
112		tcvalg 9649	. . . 4 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)})
113		r1rankidb 9720	. . . . 5 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
114		r1tr 9692	. . . . 5 ⊢ Tr (𝑅1‘(rank‘𝐴))
115		fvex 6841	. . . . . . 7 ⊢ (𝑅1‘(rank‘𝐴)) ∈ V
116		sseq2 3941	. . . . . . . 8 ⊢ (𝑥 = (𝑅1‘(rank‘𝐴)) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (𝑅1‘(rank‘𝐴))))
117		treq 5187	. . . . . . . 8 ⊢ (𝑥 = (𝑅1‘(rank‘𝐴)) → (Tr 𝑥 ↔ Tr (𝑅1‘(rank‘𝐴))))
118	116, 117	anbi12d 638	. . . . . . 7 ⊢ (𝑥 = (𝑅1‘(rank‘𝐴)) → ((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴)))))
119	115, 118	elab 3617	. . . . . 6 ⊢ ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))))
120		intss1 4894	. . . . . 6 ⊢ ((𝑅1‘(rank‘𝐴)) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
121	119, 120	sylbir 236	. . . . 5 ⊢ ((𝐴 ⊆ (𝑅1‘(rank‘𝐴)) ∧ Tr (𝑅1‘(rank‘𝐴))) → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
122	113, 114, 121	sylancl 592	. . . 4 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑅1‘(rank‘𝐴)))
123	112, 122	eqsstrd 3949	. . 3 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)))
124		imass2 6055	. . . 4 ⊢ ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank “ (𝑅1‘(rank‘𝐴))))
125		ffun 6659	. . . . . . . 8 ⊢ (rank:∪ (𝑅1 “ On)⟶On → Fun rank)
126	55, 125	ax-mp 5	. . . . . . 7 ⊢ Fun rank
127		fvelima 6893	. . . . . . 7 ⊢ ((Fun rank ∧ 𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴)))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
128	126, 127	mpan 696	. . . . . 6 ⊢ (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → ∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥)
129		rankr1ai 9714	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → (rank‘𝑦) ∈ (rank‘𝐴))
130		eleq1 2827	. . . . . . . 8 ⊢ ((rank‘𝑦) = 𝑥 → ((rank‘𝑦) ∈ (rank‘𝐴) ↔ 𝑥 ∈ (rank‘𝐴)))
131	129, 130	syl5ibcom 246	. . . . . . 7 ⊢ (𝑦 ∈ (𝑅1‘(rank‘𝐴)) → ((rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴)))
132	131	rexlimiv 3133	. . . . . 6 ⊢ (∃𝑦 ∈ (𝑅1‘(rank‘𝐴))(rank‘𝑦) = 𝑥 → 𝑥 ∈ (rank‘𝐴))
133	128, 132	syl 17	. . . . 5 ⊢ (𝑥 ∈ (rank “ (𝑅1‘(rank‘𝐴))) → 𝑥 ∈ (rank‘𝐴))
134	133	ssriv 3919	. . . 4 ⊢ (rank “ (𝑅1‘(rank‘𝐴))) ⊆ (rank‘𝐴)
135	124, 134	sstrdi 3927	. . 3 ⊢ ((TC‘𝐴) ⊆ (𝑅1‘(rank‘𝐴)) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
136	123, 135	syl 17	. 2 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank “ (TC‘𝐴)) ⊆ (rank‘𝐴))
137	111, 136	eqssd 3932	1 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = (rank “ (TC‘𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∨ w3o 1091   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  {cab 2717  ∀wral 3053  ∃wrex 3063  {crab 3391  Vcvv 3431   ⊆ wss 3883  ∪ cuni 4839  ∩ cint 4878  Tr wtr 5180   “ cima 5622  Ord word 6310  Oncon0 6311  suc csuc 6313  Fun wfun 6480   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486  TCctc 9647  𝑅₁cr1 9678  rankcrnk 9679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5200  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-inf2 9554

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-int 4879  df-iun 4924  df-br 5074  df-opab 5136  df-mpt 5155  df-tr 5181  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7360  df-om 7808  df-2nd 7933  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-tc 9648  df-r1 9680  df-rank 9681

This theorem is referenced by:  hsmexlem5  10344  grur1  10735