iss

Description: A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	iss	$⊢ A \subseteq I \leftrightarrow A = {I ↾}_{dom A}$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	opeldm	$⊢ ⟨x, y⟩ \in A \to x \in dom A$
4	3	a1i	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to x \in dom A)$
5		ssel	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to ⟨x, y⟩ \in I)$
6	4 5	jcad	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to (x \in dom A \land ⟨x, y⟩ \in I))$
7		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
8	2	ideq	$⊢ x I y \leftrightarrow x = y$
9	7 8	bitr3i	$⊢ ⟨x, y⟩ \in I \leftrightarrow x = y$
10	1	eldm2	$⊢ x \in dom A \leftrightarrow \exists y ⟨x, y⟩ \in A$
11		opeq2	$⊢ x = y \to ⟨x, x⟩ = ⟨x, y⟩$
12	11	eleq1d	$⊢ x = y \to (⟨x, x⟩ \in A \leftrightarrow ⟨x, y⟩ \in A)$
13	12	biimprcd	$⊢ ⟨x, y⟩ \in A \to (x = y \to ⟨x, x⟩ \in A)$
14	9 13	syl5bi	$⊢ ⟨x, y⟩ \in A \to (⟨x, y⟩ \in I \to ⟨x, x⟩ \in A)$
15	5 14	sylcom	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to ⟨x, x⟩ \in A)$
16	15	exlimdv	$⊢ A \subseteq I \to (\exists y ⟨x, y⟩ \in A \to ⟨x, x⟩ \in A)$
17	10 16	syl5bi	$⊢ A \subseteq I \to (x \in dom A \to ⟨x, x⟩ \in A)$
18	12	imbi2d	$⊢ x = y \to ((x \in dom A \to ⟨x, x⟩ \in A) \leftrightarrow (x \in dom A \to ⟨x, y⟩ \in A))$
19	17 18	syl5ibcom	$⊢ A \subseteq I \to (x = y \to (x \in dom A \to ⟨x, y⟩ \in A))$
20	9 19	syl5bi	$⊢ A \subseteq I \to (⟨x, y⟩ \in I \to (x \in dom A \to ⟨x, y⟩ \in A))$
21	20	impcomd	$⊢ A \subseteq I \to ((x \in dom A \land ⟨x, y⟩ \in I) \to ⟨x, y⟩ \in A)$
22	6 21	impbid	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \leftrightarrow (x \in dom A \land ⟨x, y⟩ \in I))$
23	2	opelresi	$⊢ ⟨x, y⟩ \in ({I ↾}_{dom A}) \leftrightarrow (x \in dom A \land ⟨x, y⟩ \in I)$
24	22 23	bitr4di	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{dom A}))$
25	24	alrimivv	$⊢ A \subseteq I \to \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{dom A}))$
26		reli	$⊢ Rel I$
27		relss	$⊢ A \subseteq I \to (Rel I \to Rel A)$
28	26 27	mpi	$⊢ A \subseteq I \to Rel A$
29		relres	$⊢ Rel ({I ↾}_{dom A})$
30		eqrel	$⊢ (Rel A \land Rel ({I ↾}_{dom A})) \to (A = {I ↾}_{dom A} \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{dom A})))$
31	28 29 30	sylancl	$⊢ A \subseteq I \to (A = {I ↾}_{dom A} \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{dom A})))$
32	25 31	mpbird	$⊢ A \subseteq I \to A = {I ↾}_{dom A}$
33		resss	$⊢ {I ↾}_{dom A} \subseteq I$
34		sseq1	$⊢ A = {I ↾}_{dom A} \to (A \subseteq I \leftrightarrow {I ↾}_{dom A} \subseteq I)$
35	33 34	mpbiri	$⊢ A = {I ↾}_{dom A} \to A \subseteq I$
36	32 35	impbii	$⊢ A \subseteq I \leftrightarrow A = {I ↾}_{dom A}$

Metamath Proof Explorer

Theorem iss

Proof