Theorem rnttrcl

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

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

Proof

Step	Hyp	Ref	Expression
1		df-ttrcl	⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
2	1	rneqi	⊢ ran t++ 𝑅 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
3		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) } = { 𝑦 ∣ ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
4	2 3	eqtri	⊢ ran t++ 𝑅 = { 𝑦 ∣ ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
5		fveq2	⊢ ( 𝑎 = ∪ 𝑛 → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ ∪ 𝑛 ) )
6		suceq	⊢ ( 𝑎 = ∪ 𝑛 → suc 𝑎 = suc ∪ 𝑛 )
7	6	fveq2d	⊢ ( 𝑎 = ∪ 𝑛 → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ suc ∪ 𝑛 ) )
8	5 7	breq12d	⊢ ( 𝑎 = ∪ 𝑛 → ( ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 ( 𝑓 ‘ suc ∪ 𝑛 ) ) )
9		simpr3	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
10		df-1o	⊢ 1o = suc ∅
11	10	difeq2i	⊢ ( ω ∖ 1o ) = ( ω ∖ suc ∅ )
12	11	eleq2i	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) ↔ 𝑛 ∈ ( ω ∖ suc ∅ ) )
13		peano1	⊢ ∅ ∈ ω
14		eldifsucnn	⊢ ( ∅ ∈ ω → ( 𝑛 ∈ ( ω ∖ suc ∅ ) ↔ ∃ 𝑥 ∈ ( ω ∖ ∅ ) 𝑛 = suc 𝑥 ) )
15	13 14	ax-mp	⊢ ( 𝑛 ∈ ( ω ∖ suc ∅ ) ↔ ∃ 𝑥 ∈ ( ω ∖ ∅ ) 𝑛 = suc 𝑥 )
16		dif0	⊢ ( ω ∖ ∅ ) = ω
17	16	rexeqi	⊢ ( ∃ 𝑥 ∈ ( ω ∖ ∅ ) 𝑛 = suc 𝑥 ↔ ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 )
18	12 15 17	3bitri	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) ↔ ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 )
19		nnord	⊢ ( 𝑥 ∈ ω → Ord 𝑥 )
20		ordunisuc	⊢ ( Ord 𝑥 → ∪ suc 𝑥 = 𝑥 )
21	19 20	syl	⊢ ( 𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥 )
22		vex	⊢ 𝑥 ∈ V
23	22	sucid	⊢ 𝑥 ∈ suc 𝑥
24	21 23	eqeltrdi	⊢ ( 𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥 )
25		unieq	⊢ ( 𝑛 = suc 𝑥 → ∪ 𝑛 = ∪ suc 𝑥 )
26		id	⊢ ( 𝑛 = suc 𝑥 → 𝑛 = suc 𝑥 )
27	25 26	eleq12d	⊢ ( 𝑛 = suc 𝑥 → ( ∪ 𝑛 ∈ 𝑛 ↔ ∪ suc 𝑥 ∈ suc 𝑥 ) )
28	24 27	syl5ibrcom	⊢ ( 𝑥 ∈ ω → ( 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛 ) )
29	28	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛 )
30	18 29	sylbi	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ∪ 𝑛 ∈ 𝑛 )
31	30	adantr	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∪ 𝑛 ∈ 𝑛 )
32	8 9 31	rspcdva	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 ( 𝑓 ‘ suc ∪ 𝑛 ) )
33		suceq	⊢ ( ∪ suc 𝑥 = 𝑥 → suc ∪ suc 𝑥 = suc 𝑥 )
34	21 33	syl	⊢ ( 𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥 )
35		suceq	⊢ ( ∪ 𝑛 = ∪ suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥 )
36	25 35	syl	⊢ ( 𝑛 = suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥 )
37	36 26	eqeq12d	⊢ ( 𝑛 = suc 𝑥 → ( suc ∪ 𝑛 = 𝑛 ↔ suc ∪ suc 𝑥 = suc 𝑥 ) )
38	34 37	syl5ibrcom	⊢ ( 𝑥 ∈ ω → ( 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛 ) )
39	38	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛 )
40	18 39	sylbi	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → suc ∪ 𝑛 = 𝑛 )
41	40	fveq2d	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( 𝑓 ‘ suc ∪ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
42	41	adantr	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc ∪ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
43		simpr2r	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ 𝑛 ) = 𝑦 )
44	42 43	eqtrd	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc ∪ 𝑛 ) = 𝑦 )
45	32 44	breqtrd	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 𝑦 )
46		fvex	⊢ ( 𝑓 ‘ ∪ 𝑛 ) ∈ V
47		vex	⊢ 𝑦 ∈ V
48	46 47	brelrn	⊢ ( ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 𝑦 → 𝑦 ∈ ran 𝑅 )
49	45 48	syl	⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → 𝑦 ∈ ran 𝑅 )
50	49	ex	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 ) )
51	50	exlimdv	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 ) )
52	51	rexlimiv	⊢ ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 )
53	52	exlimiv	⊢ ( ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 )
54	53	abssi	⊢ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) } ⊆ ran 𝑅
55	4 54	eqsstri	⊢ ran t++ 𝑅 ⊆ ran 𝑅
56		rnresv	⊢ ran ( 𝑅 ↾ V ) = ran 𝑅
57		relres	⊢ Rel ( 𝑅 ↾ V )
58		ssttrcl	⊢ ( Rel ( 𝑅 ↾ V ) → ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V ) )
59	57 58	ax-mp	⊢ ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V )
60		ttrclresv	⊢ t++ ( 𝑅 ↾ V ) = t++ 𝑅
61	59 60	sseqtri	⊢ ( 𝑅 ↾ V ) ⊆ t++ 𝑅
62	61	rnssi	⊢ ran ( 𝑅 ↾ V ) ⊆ ran t++ 𝑅
63	56 62	eqsstrri	⊢ ran 𝑅 ⊆ ran t++ 𝑅
64	55 63	eqssi	⊢ ran t++ 𝑅 = ran 𝑅