Theorem rnttrcl 9726

Description: The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024.)

Assertion

Ref	Expression
rnttrcl	⊢ ran t++𝑅 = ran 𝑅

Proof of Theorem rnttrcl

Dummy variables 𝑥 𝑦 𝑓 𝑛 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ttrcl 9712	. . . . 5 ⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
2	1	rneqi 5918	. . . 4 ⊢ ran t++𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
3		rnopab 5935	. . . 4 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
4	2, 3	eqtri 2783	. . 3 ⊢ ran t++𝑅 = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
5		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘𝑎) = (𝑓‘∪ 𝑛))
6		suceq 6431	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∪ 𝑛 → suc 𝑎 = suc ∪ 𝑛)
7	6	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘suc 𝑎) = (𝑓‘suc ∪ 𝑛))
8	5, 7	breq12d 5115	. . . . . . . . . . 11 ⊢ (𝑎 = ∪ 𝑛 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛)))
9		simpr3 1215	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
10		df-1o 8479	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
11	10	difeq2i 4060	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
12	11	eleq2i 2852	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
13		peano1 7900	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
14		eldifsucnn 8676	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
15	13, 14	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
16		dif0 4326	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ ∅) = ω
17	16	rexeqi 3318	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
18	12, 15, 17	3bitri 300	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
19		nnord 7885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ω → Ord 𝑥)
20		ordunisuc 7843	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 𝑥 → ∪ suc 𝑥 = 𝑥)
21	19, 20	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥)
22		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
23	22	sucid 6447	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ suc 𝑥
24	21, 23	eqeltrdi 2868	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥)
25		unieq 4877	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → ∪ 𝑛 = ∪ suc 𝑥)
26		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → 𝑛 = suc 𝑥)
27	25, 26	eleq12d 2854	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = suc 𝑥 → (∪ 𝑛 ∈ 𝑛 ↔ ∪ suc 𝑥 ∈ suc 𝑥))
28	24, 27	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛))
29	28	rexlimiv 3156	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛)
30	18, 29	sylbi 220	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → ∪ 𝑛 ∈ 𝑛)
31	30	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∪ 𝑛 ∈ 𝑛)
32	8, 9, 31	rspcdva 3577	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛))
33		suceq 6431	. . . . . . . . . . . . . . . . 17 ⊢ (∪ suc 𝑥 = 𝑥 → suc ∪ suc 𝑥 = suc 𝑥)
34	21, 33	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥)
35		suceq 6431	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑛 = ∪ suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
36	25, 35	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
37	36, 26	eqeq12d 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → (suc ∪ 𝑛 = 𝑛 ↔ suc ∪ suc 𝑥 = suc 𝑥))
38	34, 37	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛))
39	38	rexlimiv 3156	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛)
40	18, 39	sylbi 220	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) → suc ∪ 𝑛 = 𝑛)
41	40	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
42	41	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
43		simpr2r 1252	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘𝑛) = 𝑦)
44	42, 43	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = 𝑦)
45	32, 44	breqtrd 5130	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅𝑦)
46		fvex 6898	. . . . . . . . . 10 ⊢ (𝑓‘∪ 𝑛) ∈ V
47		vex 3454	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
48	46, 47	brelrn 5923	. . . . . . . . 9 ⊢ ((𝑓‘∪ 𝑛)𝑅𝑦 → 𝑦 ∈ ran 𝑅)
49	45, 48	syl 18	. . . . . . . 8 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑦 ∈ ran 𝑅)
50	49	ex 418	. . . . . . 7 ⊢ (𝑛 ∈ (ω ∖ 1o) → ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅))
51	50	exlimdv 1965	. . . . . 6 ⊢ (𝑛 ∈ (ω ∖ 1o) → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅))
52	51	rexlimiv 3156	. . . . 5 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
53	52	exlimiv 1962	. . . 4 ⊢ (∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
54	53	abssi 3993	. . 3 ⊢ {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} ⊆ ran 𝑅
55	4, 54	eqsstri 3954	. 2 ⊢ ran t++𝑅 ⊆ ran 𝑅
56		rnresv 6195	. . 3 ⊢ ran (𝑅 ↾ V) = ran 𝑅
57		relres 5995	. . . . . 6 ⊢ Rel (𝑅 ↾ V)
58		ssttrcl 9719	. . . . . 6 ⊢ (Rel (𝑅 ↾ V) → (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V))
59	57, 58	ax-mp 5	. . . . 5 ⊢ (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V)
60		ttrclresv 9721	. . . . 5 ⊢ t++(𝑅 ↾ V) = t++𝑅
61	59, 60	sseqtri 3956	. . . 4 ⊢ (𝑅 ↾ V) ⊆ t++𝑅
62	61	rnssi 5921	. . 3 ⊢ ran (𝑅 ↾ V) ⊆ ran t++𝑅
63	56, 62	eqsstrri 3955	. 2 ⊢ ran 𝑅 ⊆ ran t++𝑅
64	55, 63	eqssi 3924	1 ⊢ ran t++𝑅 = ran 𝑅

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045  ∅c0 4278  ∪ cuni 4866   class class class wbr 5102  {copab 5166  ran crn 5651   ↾ cres 5652  Rel wrel 5655  Ord word 6361  suc csuc 6364   Fn wfn 6533  ‘cfv 6538  ωcom 7877  1_oc1o 8472  t++cttrcl 9711

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-oadd 8483  df-ttrcl 9712

This theorem is used by:  ttrclexg  9727