Theorem rnttrcl 9682

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 9668	. . . . 5 ⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
2	1	rneqi 5904	. . . 4 ⊢ ran t++𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
3		rnopab 5921	. . . 4 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
4	2, 3	eqtri 2753	. . 3 ⊢ ran t++𝑅 = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
5		fveq2 6861	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘𝑎) = (𝑓‘∪ 𝑛))
6		suceq 6403	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∪ 𝑛 → suc 𝑎 = suc ∪ 𝑛)
7	6	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘suc 𝑎) = (𝑓‘suc ∪ 𝑛))
8	5, 7	breq12d 5123	. . . . . . . . . . 11 ⊢ (𝑎 = ∪ 𝑛 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛)))
9		simpr3 1197	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
10		df-1o 8437	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
11	10	difeq2i 4089	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
12	11	eleq2i 2821	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
13		peano1 7868	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
14		eldifsucnn 8631	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
15	13, 14	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
16		dif0 4344	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ ∅) = ω
17	16	rexeqi 3300	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
18	12, 15, 17	3bitri 297	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
19		nnord 7853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ω → Ord 𝑥)
20		ordunisuc 7810	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 𝑥 → ∪ suc 𝑥 = 𝑥)
21	19, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥)
22		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
23	22	sucid 6419	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ suc 𝑥
24	21, 23	eqeltrdi 2837	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥)
25		unieq 4885	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → ∪ 𝑛 = ∪ suc 𝑥)
26		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → 𝑛 = suc 𝑥)
27	25, 26	eleq12d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = suc 𝑥 → (∪ 𝑛 ∈ 𝑛 ↔ ∪ suc 𝑥 ∈ suc 𝑥))
28	24, 27	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛))
29	28	rexlimiv 3128	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛)
30	18, 29	sylbi 217	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → ∪ 𝑛 ∈ 𝑛)
31	30	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∪ 𝑛 ∈ 𝑛)
32	8, 9, 31	rspcdva 3592	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛))
33		suceq 6403	. . . . . . . . . . . . . . . . 17 ⊢ (∪ suc 𝑥 = 𝑥 → suc ∪ suc 𝑥 = suc 𝑥)
34	21, 33	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥)
35		suceq 6403	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑛 = ∪ suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
36	25, 35	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
37	36, 26	eqeq12d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → (suc ∪ 𝑛 = 𝑛 ↔ suc ∪ suc 𝑥 = suc 𝑥))
38	34, 37	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛))
39	38	rexlimiv 3128	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛)
40	18, 39	sylbi 217	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) → suc ∪ 𝑛 = 𝑛)
41	40	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
42	41	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
43		simpr2r 1234	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘𝑛) = 𝑦)
44	42, 43	eqtrd 2765	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = 𝑦)
45	32, 44	breqtrd 5136	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅𝑦)
46		fvex 6874	. . . . . . . . . 10 ⊢ (𝑓‘∪ 𝑛) ∈ V
47		vex 3454	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
48	46, 47	brelrn 5909	. . . . . . . . 9 ⊢ ((𝑓‘∪ 𝑛)𝑅𝑦 → 𝑦 ∈ ran 𝑅)
49	45, 48	syl 17	. . . . . . . 8 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑦 ∈ ran 𝑅)
50	49	ex 412	. . . . . . 7 ⊢ (𝑛 ∈ (ω ∖ 1o) → ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅))
51	50	exlimdv 1933	. . . . . 6 ⊢ (𝑛 ∈ (ω ∖ 1o) → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅))
52	51	rexlimiv 3128	. . . . 5 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
53	52	exlimiv 1930	. . . 4 ⊢ (∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
54	53	abssi 4036	. . 3 ⊢ {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} ⊆ ran 𝑅
55	4, 54	eqsstri 3996	. 2 ⊢ ran t++𝑅 ⊆ ran 𝑅
56		rnresv 6177	. . 3 ⊢ ran (𝑅 ↾ V) = ran 𝑅
57		relres 5979	. . . . . 6 ⊢ Rel (𝑅 ↾ V)
58		ssttrcl 9675	. . . . . 6 ⊢ (Rel (𝑅 ↾ V) → (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V))
59	57, 58	ax-mp 5	. . . . 5 ⊢ (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V)
60		ttrclresv 9677	. . . . 5 ⊢ t++(𝑅 ↾ V) = t++𝑅
61	59, 60	sseqtri 3998	. . . 4 ⊢ (𝑅 ↾ V) ⊆ t++𝑅
62	61	rnssi 5907	. . 3 ⊢ ran (𝑅 ↾ V) ⊆ ran t++𝑅
63	56, 62	eqsstrri 3997	. 2 ⊢ ran 𝑅 ⊆ ran t++𝑅
64	55, 63	eqssi 3966	1 ⊢ ran t++𝑅 = ran 𝑅

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2708  ∀wral 3045  ∃wrex 3054  Vcvv 3450   ∖ cdif 3914   ⊆ wss 3917  ∅c0 4299  ∪ cuni 4874   class class class wbr 5110  {copab 5172  ran crn 5642   ↾ cres 5643  Rel wrel 5646  Ord word 6334  suc csuc 6337   Fn wfn 6509  ‘cfv 6514  ωcom 7845  1_oc1o 8430  t++cttrcl 9667

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 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-oadd 8441  df-ttrcl 9668

This theorem is referenced by:  ttrclexg  9683