Theorem rnttrcl 9717

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 9703	. . . . 5 ⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
2	1	rneqi 5937	. . . 4 ⊢ ran t++𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
3		rnopab 5954	. . . 4 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
4	2, 3	eqtri 2761	. . 3 ⊢ ran t++𝑅 = {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))}
5		fveq2 6892	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘𝑎) = (𝑓‘∪ 𝑛))
6		suceq 6431	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∪ 𝑛 → suc 𝑎 = suc ∪ 𝑛)
7	6	fveq2d 6896	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑛 → (𝑓‘suc 𝑎) = (𝑓‘suc ∪ 𝑛))
8	5, 7	breq12d 5162	. . . . . . . . . . 11 ⊢ (𝑎 = ∪ 𝑛 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛)))
9		simpr3 1197	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
10		df-1o 8466	. . . . . . . . . . . . . . . 16 ⊢ 1o = suc ∅
11	10	difeq2i 4120	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ 1o) = (ω ∖ suc ∅)
12	11	eleq2i 2826	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ 𝑛 ∈ (ω ∖ suc ∅))
13		peano1 7879	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
14		eldifsucnn 8663	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ ω → (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥))
15	13, 14	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ω ∖ suc ∅) ↔ ∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥)
16		dif0 4373	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ ∅) = ω
17	16	rexeqi 3325	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ (ω ∖ ∅)𝑛 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
18	12, 15, 17	3bitri 297	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) ↔ ∃𝑥 ∈ ω 𝑛 = suc 𝑥)
19		nnord 7863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ω → Ord 𝑥)
20		ordunisuc 7820	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 𝑥 → ∪ suc 𝑥 = 𝑥)
21	19, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥)
22		vex 3479	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
23	22	sucid 6447	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ suc 𝑥
24	21, 23	eqeltrdi 2842	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥)
25		unieq 4920	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → ∪ 𝑛 = ∪ suc 𝑥)
26		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → 𝑛 = suc 𝑥)
27	25, 26	eleq12d 2828	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = suc 𝑥 → (∪ 𝑛 ∈ 𝑛 ↔ ∪ suc 𝑥 ∈ suc 𝑥))
28	24, 27	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛))
29	28	rexlimiv 3149	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛)
30	18, 29	sylbi 216	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → ∪ 𝑛 ∈ 𝑛)
31	30	adantr 482	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∪ 𝑛 ∈ 𝑛)
32	8, 9, 31	rspcdva 3614	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅(𝑓‘suc ∪ 𝑛))
33		suceq 6431	. . . . . . . . . . . . . . . . 17 ⊢ (∪ suc 𝑥 = 𝑥 → suc ∪ suc 𝑥 = suc 𝑥)
34	21, 33	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥)
35		suceq 6431	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑛 = ∪ suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
36	25, 35	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥)
37	36, 26	eqeq12d 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = suc 𝑥 → (suc ∪ 𝑛 = 𝑛 ↔ suc ∪ suc 𝑥 = suc 𝑥))
38	34, 37	syl5ibrcom 246	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → (𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛))
39	38	rexlimiv 3149	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛)
40	18, 39	sylbi 216	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ω ∖ 1o) → suc ∪ 𝑛 = 𝑛)
41	40	fveq2d 6896	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ω ∖ 1o) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
42	41	adantr 482	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = (𝑓‘𝑛))
43		simpr2r 1234	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘𝑛) = 𝑦)
44	42, 43	eqtrd 2773	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc ∪ 𝑛) = 𝑦)
45	32, 44	breqtrd 5175	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∪ 𝑛)𝑅𝑦)
46		fvex 6905	. . . . . . . . . 10 ⊢ (𝑓‘∪ 𝑛) ∈ V
47		vex 3479	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
48	46, 47	brelrn 5942	. . . . . . . . 9 ⊢ ((𝑓‘∪ 𝑛)𝑅𝑦 → 𝑦 ∈ ran 𝑅)
49	45, 48	syl 17	. . . . . . . 8 ⊢ ((𝑛 ∈ (ω ∖ 1o) ∧ (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑦 ∈ ran 𝑅)
50	49	ex 414	. . . . . . 7 ⊢ (𝑛 ∈ (ω ∖ 1o) → ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅))
51	50	exlimdv 1937	. . . . . 6 ⊢ (𝑛 ∈ (ω ∖ 1o) → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅))
52	51	rexlimiv 3149	. . . . 5 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
53	52	exlimiv 1934	. . . 4 ⊢ (∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑦 ∈ ran 𝑅)
54	53	abssi 4068	. . 3 ⊢ {𝑦 ∣ ∃𝑥∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))} ⊆ ran 𝑅
55	4, 54	eqsstri 4017	. 2 ⊢ ran t++𝑅 ⊆ ran 𝑅
56		rnresv 6201	. . 3 ⊢ ran (𝑅 ↾ V) = ran 𝑅
57		relres 6011	. . . . . 6 ⊢ Rel (𝑅 ↾ V)
58		ssttrcl 9710	. . . . . 6 ⊢ (Rel (𝑅 ↾ V) → (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V))
59	57, 58	ax-mp 5	. . . . 5 ⊢ (𝑅 ↾ V) ⊆ t++(𝑅 ↾ V)
60		ttrclresv 9712	. . . . 5 ⊢ t++(𝑅 ↾ V) = t++𝑅
61	59, 60	sseqtri 4019	. . . 4 ⊢ (𝑅 ↾ V) ⊆ t++𝑅
62	61	rnssi 5940	. . 3 ⊢ ran (𝑅 ↾ V) ⊆ ran t++𝑅
63	56, 62	eqsstrri 4018	. 2 ⊢ ran 𝑅 ⊆ ran t++𝑅
64	55, 63	eqssi 3999	1 ⊢ ran t++𝑅 = ran 𝑅

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  ∃wex 1782   ∈ wcel 2107  {cab 2710  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∖ cdif 3946   ⊆ wss 3949  ∅c0 4323  ∪ cuni 4909   class class class wbr 5149  {copab 5211  ran crn 5678   ↾ cres 5679  Rel wrel 5682  Ord word 6364  suc csuc 6367   Fn wfn 6539  ‘cfv 6544  ωcom 7855  1_oc1o 8459  t++cttrcl 9702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-ttrcl 9703

This theorem is referenced by:  ttrclexg  9718