Theorem rncoOLD

Description: Obsolete version of rnco as of 24-Jan-2026. (Contributed by NM, 12-Dec-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	brco	⊢ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
4	3	exbii	⊢ ( ∃ 𝑥 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑥 ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
5		excom	⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
6		vex	⊢ 𝑧 ∈ V
7	6	elrn	⊢ ( 𝑧 ∈ ran 𝐵 ↔ ∃ 𝑥 𝑥 𝐵 𝑧 )
8	7	anbi1i	⊢ ( ( 𝑧 ∈ ran 𝐵 ∧ 𝑧 𝐴 𝑦 ) ↔ ( ∃ 𝑥 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
9	2	brresi	⊢ ( 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 ↔ ( 𝑧 ∈ ran 𝐵 ∧ 𝑧 𝐴 𝑦 ) )
10		19.41v	⊢ ( ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( ∃ 𝑥 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
11	8 9 10	3bitr4ri	⊢ ( ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
12	11	exbii	⊢ ( ∃ 𝑧 ∃ 𝑥 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
13	4 5 12	3bitri	⊢ ( ∃ 𝑥 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
14	2	elrn	⊢ ( 𝑦 ∈ ran ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 )
15	2	elrn	⊢ ( 𝑦 ∈ ran ( 𝐴 ↾ ran 𝐵 ) ↔ ∃ 𝑧 𝑧 ( 𝐴 ↾ ran 𝐵 ) 𝑦 )
16	13 14 15	3bitr4i	⊢ ( 𝑦 ∈ ran ( 𝐴 ∘ 𝐵 ) ↔ 𝑦 ∈ ran ( 𝐴 ↾ ran 𝐵 ) )
17	16	eqriv	⊢ ran ( 𝐴 ∘ 𝐵 ) = ran ( 𝐴 ↾ ran 𝐵 )