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 ⁡ A ∘ B = ran ⁡ A ↾ ran ⁡ B

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 vex ⊢ y ∈ V
3 1 2 brco ⊢ x A ∘ B y ↔ ∃ z x B z ∧ z A y
4 3 exbii ⊢ ∃ x x A ∘ B y ↔ ∃ x ∃ z x B z ∧ z A y
5 breq1 ⊢ x = w → x B z ↔ w B z
6 5 anbi1d ⊢ x = w → x B z ∧ z A y ↔ w B z ∧ z A y
7 breq2 ⊢ z = w → x B z ↔ x B w
8 breq1 ⊢ z = w → z A y ↔ w A y
9 7 8 anbi12d ⊢ z = w → x B z ∧ z A y ↔ x B w ∧ w A y
10 6 9 excomw ⊢ ∃ x ∃ z x B z ∧ z A y ↔ ∃ z ∃ x x B z ∧ z A y
11 vex ⊢ z ∈ V
12 11 elrn ⊢ z ∈ ran ⁡ B ↔ ∃ x x B z
13 12 anbi1i ⊢ z ∈ ran ⁡ B ∧ z A y ↔ ∃ x x B z ∧ z A y
14 2 brresi ⊢ z A ↾ ran ⁡ B y ↔ z ∈ ran ⁡ B ∧ z A y
15 19.41v ⊢ ∃ x x B z ∧ z A y ↔ ∃ x x B z ∧ z A y
16 13 14 15 3bitr4ri ⊢ ∃ x x B z ∧ z A y ↔ z A ↾ ran ⁡ B y
17 16 exbii ⊢ ∃ z ∃ x x B z ∧ z A y ↔ ∃ z z A ↾ ran ⁡ B y
18 4 10 17 3bitri ⊢ ∃ x x A ∘ B y ↔ ∃ z z A ↾ ran ⁡ B y
19 2 elrn ⊢ y ∈ ran ⁡ A ∘ B ↔ ∃ x x A ∘ B y
20 2 elrn ⊢ y ∈ ran ⁡ A ↾ ran ⁡ B ↔ ∃ z z A ↾ ran ⁡ B y
21 18 19 20 3bitr4i ⊢ y ∈ ran ⁡ A ∘ B ↔ y ∈ ran ⁡ A ↾ ran ⁡ B
22 21 eqriv ⊢ ran ⁡ A ∘ B = ran ⁡ A ↾ ran ⁡ B