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	$⊢ B \subseteq ran ({C ↾}_{A}) \leftrightarrow ran (C \cap (A \times B)) = B$

Proof

Step	Hyp	Ref	Expression
1		inss2	$⊢ C \cap (A \times B) \subseteq A \times B$
2	1	rnssi	$⊢ ran (C \cap (A \times B)) \subseteq ran (A \times B)$
3		rnxpss	$⊢ ran (A \times B) \subseteq B$
4	2 3	sstri	$⊢ ran (C \cap (A \times B)) \subseteq B$
5		eqss	$⊢ ran (C \cap (A \times B)) = B \leftrightarrow (ran (C \cap (A \times B)) \subseteq B \land B \subseteq ran (C \cap (A \times B)))$
6	4 5	mpbiran	$⊢ ran (C \cap (A \times B)) = B \leftrightarrow B \subseteq ran (C \cap (A \times B))$
7		inxpssres	$⊢ C \cap (A \times B) \subseteq {C ↾}_{A}$
8	7	rnssi	$⊢ ran (C \cap (A \times B)) \subseteq ran ({C ↾}_{A})$
9		sstr	$⊢ (B \subseteq ran (C \cap (A \times B)) \land ran (C \cap (A \times B)) \subseteq ran ({C ↾}_{A})) \to B \subseteq ran ({C ↾}_{A})$
10	8 9	mpan2	$⊢ B \subseteq ran (C \cap (A \times B)) \to B \subseteq ran ({C ↾}_{A})$
11		ssel	$⊢ B \subseteq ran ({C ↾}_{A}) \to (y \in B \to y \in ran ({C ↾}_{A}))$
12		vex	$⊢ y \in V$
13	12	elrn2	$⊢ y \in ran ({C ↾}_{A}) \leftrightarrow \exists x ⟨x, y⟩ \in ({C ↾}_{A})$
14	11 13	imbitrdi	$⊢ B \subseteq ran ({C ↾}_{A}) \to (y \in B \to \exists x ⟨x, y⟩ \in ({C ↾}_{A}))$
15	14	ancld	$⊢ B \subseteq ran ({C ↾}_{A}) \to (y \in B \to (y \in B \land \exists x ⟨x, y⟩ \in ({C ↾}_{A})))$
16	12	elrn2	$⊢ y \in ran (C \cap (A \times B)) \leftrightarrow \exists x ⟨x, y⟩ \in (C \cap (A \times B))$
17		opelinxp	$⊢ ⟨x, y⟩ \in (C \cap (A \times B)) \leftrightarrow ((x \in A \land y \in B) \land ⟨x, y⟩ \in C)$
18	12	opelresi	$⊢ ⟨x, y⟩ \in ({C ↾}_{A}) \leftrightarrow (x \in A \land ⟨x, y⟩ \in C)$
19	18	bianassc	$⊢ (y \in B \land ⟨x, y⟩ \in ({C ↾}_{A})) \leftrightarrow ((x \in A \land y \in B) \land ⟨x, y⟩ \in C)$
20	17 19	bitr4i	$⊢ ⟨x, y⟩ \in (C \cap (A \times B)) \leftrightarrow (y \in B \land ⟨x, y⟩ \in ({C ↾}_{A}))$
21	20	exbii	$⊢ \exists x ⟨x, y⟩ \in (C \cap (A \times B)) \leftrightarrow \exists x (y \in B \land ⟨x, y⟩ \in ({C ↾}_{A}))$
22		19.42v	$⊢ \exists x (y \in B \land ⟨x, y⟩ \in ({C ↾}_{A})) \leftrightarrow (y \in B \land \exists x ⟨x, y⟩ \in ({C ↾}_{A}))$
23	16 21 22	3bitri	$⊢ y \in ran (C \cap (A \times B)) \leftrightarrow (y \in B \land \exists x ⟨x, y⟩ \in ({C ↾}_{A}))$
24	15 23	imbitrrdi	$⊢ B \subseteq ran ({C ↾}_{A}) \to (y \in B \to y \in ran (C \cap (A \times B)))$
25	24	ssrdv	$⊢ B \subseteq ran ({C ↾}_{A}) \to B \subseteq ran (C \cap (A \times B))$
26	10 25	impbii	$⊢ B \subseteq ran (C \cap (A \times B)) \leftrightarrow B \subseteq ran ({C ↾}_{A})$
27	6 26	bitr2i	$⊢ B \subseteq ran ({C ↾}_{A}) \leftrightarrow ran (C \cap (A \times B)) = B$

Metamath Proof Explorer

Theorem ssrnres

Proof