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

Metamath Proof Explorer

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