Theorem rnttrcl 9741

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 9727	. . . . 5 ⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
2	1	rneqi 5922	. . . 4 ⊢ ran t++𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
3		rnopab 5939	. . . 4 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
4	2, 3	eqtri 2759	. . 3 ⊢ ran t++𝑅 = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
5		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘𝑎) = (𝑓‘∪ 𝑛))
6		suceq 6424	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∪ 𝑛 → suc 𝑎 = suc ∪ 𝑛)
7	6	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘suc 𝑎) = (𝑓‘suc ∪ 𝑛))
8	5, 7	breq12d 5137	. . . . . . . . . . 11 ⊢ (𝑎 = ∪ 𝑛 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛)))
9		simpr3 1197	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
10		df-1o 8485	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
11	10	difeq2i 4103	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
12	11	eleq2i 2827	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
13		peano1 7889	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
14		eldifsucnn 8681	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
15	13, 14	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
16		dif0 4358	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ ∅) = ω
17	16	rexeqi 3308	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
18	12, 15, 17	3bitri 297	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
19		nnord 7874	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ω → Ord 𝑥)
20		ordunisuc 7831	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 𝑥 → ∪ suc 𝑥 = 𝑥)
21	19, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥)
22		vex 3468	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
23	22	sucid 6441	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ suc 𝑥
24	21, 23	eqeltrdi 2843	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥)
25		unieq 4899	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → ∪ 𝑛 = ∪ suc 𝑥)
26		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → 𝑛 = suc 𝑥)
27	25, 26	eleq12d 2829	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = suc 𝑥 → (∪ 𝑛 ∈ 𝑛 ↔ ∪ suc 𝑥 ∈ suc 𝑥))
28	24, 27	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛))
29	28	rexlimiv 3135	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛)
30	18, 29	sylbi 217	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → ∪ 𝑛 ∈ 𝑛)
31	30	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∪ 𝑛 ∈ 𝑛)
32	8, 9, 31	rspcdva 3607	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛))
33		suceq 6424	. . . . . . . . . . . . . . . . 17 ⊢ (∪ suc 𝑥 = 𝑥 → suc ∪ suc 𝑥 = suc 𝑥)
34	21, 33	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥)
35		suceq 6424	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑛 = ∪ suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
36	25, 35	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
37	36, 26	eqeq12d 2752	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → (suc ∪ 𝑛 = 𝑛 ↔ suc ∪ suc 𝑥 = suc 𝑥))
38	34, 37	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛))
39	38	rexlimiv 3135	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛)
40	18, 39	sylbi 217	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) → suc ∪ 𝑛 = 𝑛)
41	40	fveq2d 6885	. . . . . . . . . . . 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 2771	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = 𝑦)
45	32, 44	breqtrd 5150	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅𝑦)
46		fvex 6894	. . . . . . . . . 10 ⊢ (𝑓‘∪ 𝑛) ∈ V
47		vex 3468	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
48	46, 47	brelrn 5927	. . . . . . . . 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 3135	. . . . 5 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
53	52	exlimiv 1930	. . . 4 ⊢ (∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
54	53	abssi 4050	. . 3 ⊢ {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} ⊆ ran 𝑅
55	4, 54	eqsstri 4010	. 2 ⊢ ran t++𝑅 ⊆ ran 𝑅
56		rnresv 6195	. . 3 ⊢ ran (𝑅 ↾ V) = ran 𝑅
57		relres 5997	. . . . . 6 ⊢ Rel (𝑅 ↾ V)
58		ssttrcl 9734	. . . . . 6 ⊢ (Rel (𝑅 ↾ V) → (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V))
59	57, 58	ax-mp 5	. . . . 5 ⊢ (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V)
60		ttrclresv 9736	. . . . 5 ⊢ t++(𝑅 ↾ V) = t++𝑅
61	59, 60	sseqtri 4012	. . . 4 ⊢ (𝑅 ↾ V) ⊆ t++𝑅
62	61	rnssi 5925	. . 3 ⊢ ran (𝑅 ↾ V) ⊆ ran t++𝑅
63	56, 62	eqsstrri 4011	. 2 ⊢ ran 𝑅 ⊆ ran t++𝑅
64	55, 63	eqssi 3980	1 ⊢ ran t++𝑅 = ran 𝑅

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714  ∀wral 3052  ∃wrex 3061  Vcvv 3464   ∖ cdif 3928   ⊆ wss 3931  ∅c0 4313  ∪ cuni 4888   class class class wbr 5124  {copab 5186  ran crn 5660   ↾ cres 5661  Rel wrel 5664  Ord word 6356  suc csuc 6359   Fn wfn 6531  ‘cfv 6536  ωcom 7866  1_oc1o 8478  t++cttrcl 9726

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 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-oadd 8489  df-ttrcl 9727

This theorem is referenced by:  ttrclexg  9742