Theorem rnttrcl 9791

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 9777	. . . . 5 ⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
2	1	rneqi 5962	. . . 4 ⊢ ran t++𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
3		rnopab 5979	. . . 4 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
4	2, 3	eqtri 2768	. . 3 ⊢ ran t++𝑅 = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
5		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘𝑎) = (𝑓‘∪ 𝑛))
6		suceq 6461	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∪ 𝑛 → suc 𝑎 = suc ∪ 𝑛)
7	6	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘suc 𝑎) = (𝑓‘suc ∪ 𝑛))
8	5, 7	breq12d 5179	. . . . . . . . . . 11 ⊢ (𝑎 = ∪ 𝑛 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛)))
9		simpr3 1196	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
10		df-1o 8522	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
11	10	difeq2i 4146	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
12	11	eleq2i 2836	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
13		peano1 7927	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
14		eldifsucnn 8720	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
15	13, 14	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
16		dif0 4400	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ ∅) = ω
17	16	rexeqi 3333	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
18	12, 15, 17	3bitri 297	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
19		nnord 7911	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ω → Ord 𝑥)
20		ordunisuc 7868	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 𝑥 → ∪ suc 𝑥 = 𝑥)
21	19, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥)
22		vex 3492	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
23	22	sucid 6477	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ suc 𝑥
24	21, 23	eqeltrdi 2852	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥)
25		unieq 4942	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → ∪ 𝑛 = ∪ suc 𝑥)
26		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → 𝑛 = suc 𝑥)
27	25, 26	eleq12d 2838	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = suc 𝑥 → (∪ 𝑛 ∈ 𝑛 ↔ ∪ suc 𝑥 ∈ suc 𝑥))
28	24, 27	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛))
29	28	rexlimiv 3154	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛)
30	18, 29	sylbi 217	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → ∪ 𝑛 ∈ 𝑛)
31	30	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∪ 𝑛 ∈ 𝑛)
32	8, 9, 31	rspcdva 3636	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛))
33		suceq 6461	. . . . . . . . . . . . . . . . 17 ⊢ (∪ suc 𝑥 = 𝑥 → suc ∪ suc 𝑥 = suc 𝑥)
34	21, 33	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥)
35		suceq 6461	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑛 = ∪ suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
36	25, 35	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
37	36, 26	eqeq12d 2756	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → (suc ∪ 𝑛 = 𝑛 ↔ suc ∪ suc 𝑥 = suc 𝑥))
38	34, 37	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛))
39	38	rexlimiv 3154	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛)
40	18, 39	sylbi 217	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) → suc ∪ 𝑛 = 𝑛)
41	40	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
42	41	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
43		simpr2r 1233	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘𝑛) = 𝑦)
44	42, 43	eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = 𝑦)
45	32, 44	breqtrd 5192	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅𝑦)
46		fvex 6933	. . . . . . . . . 10 ⊢ (𝑓‘∪ 𝑛) ∈ V
47		vex 3492	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
48	46, 47	brelrn 5967	. . . . . . . . 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 1932	. . . . . 6 ⊢ (𝑛 ∈ (ω ∖ 1o) → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅))
52	51	rexlimiv 3154	. . . . 5 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
53	52	exlimiv 1929	. . . 4 ⊢ (∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
54	53	abssi 4093	. . 3 ⊢ {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} ⊆ ran 𝑅
55	4, 54	eqsstri 4043	. 2 ⊢ ran t++𝑅 ⊆ ran 𝑅
56		rnresv 6232	. . 3 ⊢ ran (𝑅 ↾ V) = ran 𝑅
57		relres 6035	. . . . . 6 ⊢ Rel (𝑅 ↾ V)
58		ssttrcl 9784	. . . . . 6 ⊢ (Rel (𝑅 ↾ V) → (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V))
59	57, 58	ax-mp 5	. . . . 5 ⊢ (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V)
60		ttrclresv 9786	. . . . 5 ⊢ t++(𝑅 ↾ V) = t++𝑅
61	59, 60	sseqtri 4045	. . . 4 ⊢ (𝑅 ↾ V) ⊆ t++𝑅
62	61	rnssi 5965	. . 3 ⊢ ran (𝑅 ↾ V) ⊆ ran t++𝑅
63	56, 62	eqsstrri 4044	. 2 ⊢ ran 𝑅 ⊆ ran t++𝑅
64	55, 63	eqssi 4025	1 ⊢ ran t++𝑅 = ran 𝑅

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537  ∃wex 1777   ∈ wcel 2108  {cab 2717  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∖ cdif 3973   ⊆ wss 3976  ∅c0 4352  ∪ cuni 4931   class class class wbr 5166  {copab 5228  ran crn 5701   ↾ cres 5702  Rel wrel 5705  Ord word 6394  suc csuc 6397   Fn wfn 6568  ‘cfv 6573  ωcom 7903  1_oc1o 8515  t++cttrcl 9776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-oadd 8526  df-ttrcl 9777

This theorem is referenced by:  ttrclexg  9792