Metamath Proof Explorer

Theorem ssrnres

Description: Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product): the LHS expresses inclusion in the range of the restricted relation, while the RHS expresses equality with the range of the restricted and corestricted relation. (Contributed by NM, 16-Jan-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion ssrnres ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) ↔ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 inss2 ⊢ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 )
2 1 rnssi ⊢ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ran ( 𝐴 × 𝐵 )
3 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
4 2 3 sstri ⊢ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝐵
5 eqss ⊢ ( ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ ( ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ) )
6 4 5 mpbiran ⊢ ( ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ 𝐵 ⊆ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) )
7 inxpssres ⊢ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐶 ↾ 𝐴 )
8 7 rnssi ⊢ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ran ( 𝐶 ↾ 𝐴 )
9 sstr ⊢ ( ( 𝐵 ⊆ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ∧ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ran ( 𝐶 ↾ 𝐴 ) ) → 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) )
10 8 9 mpan2 ⊢ ( 𝐵 ⊆ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) → 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) )
11 ssel ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ran ( 𝐶 ↾ 𝐴 ) ) )
12 vex ⊢ 𝑦 ∈ V
13 12 elrn2 ⊢ ( 𝑦 ∈ ran ( 𝐶 ↾ 𝐴 ) ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) )
14 11 13 imbitrdi ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) )
15 14 ancld ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) ) )
16 12 elrn2 ⊢ ( 𝑦 ∈ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) )
17 opelinxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ) )
18 12 opelresi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ) )
19 18 bianassc ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐶 ) )
20 17 19 bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) )
21 20 exbii ⊢ ( ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) )
22 19.42v ⊢ ( ∃ 𝑥 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) )
23 16 21 22 3bitri ⊢ ( 𝑦 ∈ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ↾ 𝐴 ) ) )
24 15 23 imbitrrdi ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ) )
25 24 ssrdv ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) → 𝐵 ⊆ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) )
26 10 25 impbii ⊢ ( 𝐵 ⊆ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) ↔ 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) )
27 6 26 bitr2i ⊢ ( 𝐵 ⊆ ran ( 𝐶 ↾ 𝐴 ) ↔ ran ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 )