This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 )