Theorem rnco

Description: The range of the composition of two classes. (Contributed by NM, 12-Dec-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022) Avoid ax-11 . (Revised by TM, 24-Jan-2026)

	Ref	Expression
Assertion	rnco	⊢ ran ( 𝐴 ∘ 𝐵 ) = ran ( 𝐴 ↾ ran 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	brco	⊢ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
4	3	exbii	⊢ ( ∃ 𝑥 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑥 ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
5		breq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐵 𝑧 ↔ 𝑤 𝐵 𝑧 ) )
6	5	anbi1d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑤 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
7		breq2	⊢ ( 𝑧 = 𝑤 → ( 𝑥 𝐵 𝑧 ↔ 𝑥 𝐵 𝑤 ) )
8		breq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 𝐴 𝑦 ↔ 𝑤 𝐴 𝑦 ) )
9	7 8	anbi12d	⊢ ( 𝑧 = 𝑤 → ( ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑥 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
10	6 9	excomw	⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
11		vex	⊢ 𝑧 ∈ V
12	11	elrn	⊢ ( 𝑧 ∈ ran 𝐵 ↔ ∃ 𝑥 𝑥 𝐵 𝑧 )
13	12	anbi1i	⊢ ( ( 𝑧 ∈ ran 𝐵 ∧ 𝑧 𝐴 𝑦 ) ↔ ( ∃ 𝑥 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
14	2	brresi	⊢ ( 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 ↔ ( 𝑧 ∈ ran 𝐵 ∧ 𝑧 𝐴 𝑦 ) )
15		19.41v	⊢ ( ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( ∃ 𝑥 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
16	13 14 15	3bitr4ri	⊢ ( ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
17	16	exbii	⊢ ( ∃ 𝑧 ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
18	4 10 17	3bitri	⊢ ( ∃ 𝑥 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
19	2	elrn	⊢ ( 𝑦 ∈ ran ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 )
20	2	elrn	⊢ ( 𝑦 ∈ ran ( 𝐴 ↾ ran 𝐵 ) ↔ ∃ 𝑧 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
21	18 19 20	3bitr4i	⊢ ( 𝑦 ∈ ran ( 𝐴 ∘ 𝐵 ) ↔ 𝑦 ∈ ran ( 𝐴 ↾ ran 𝐵 ) )
22	21	eqriv	⊢ ran ( 𝐴 ∘ 𝐵 ) = ran ( 𝐴 ↾ ran 𝐵 )