Theorem 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	⊢ ( 𝐴 ⊆ I ↔ 𝐴 = ( I ↾ dom 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	opeldm	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 )
4	3	a1i	⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 ) )
5		ssel	⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
6	4 5	jcad	⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ) )
7		df-br	⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
8	2	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
9	7 8	bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑥 = 𝑦 )
10	1	eldm2	⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
11		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
12	11	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
13	12	biimprcd	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
14	9 13	syl5bi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
15	5 14	sylcom	⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
16	15	exlimdv	⊢ ( 𝐴 ⊆ I → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
17	10 16	syl5bi	⊢ ( 𝐴 ⊆ I → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
18	12	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
19	17 18	syl5ibcom	⊢ ( 𝐴 ⊆ I → ( 𝑥 = 𝑦 → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
20	9 19	syl5bi	⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
21	20	impcomd	⊢ ( 𝐴 ⊆ I → ( ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
22	6 21	impbid	⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ) )
23	2	opelresi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ dom 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
24	22 23	bitr4di	⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ dom 𝐴 ) ) )
25	24	alrimivv	⊢ ( 𝐴 ⊆ I → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ dom 𝐴 ) ) )
26		reli	⊢ Rel I
27		relss	⊢ ( 𝐴 ⊆ I → ( Rel I → Rel 𝐴 ) )
28	26 27	mpi	⊢ ( 𝐴 ⊆ I → Rel 𝐴 )
29		relres	⊢ Rel ( I ↾ dom 𝐴 )
30		eqrel	⊢ ( ( Rel 𝐴 ∧ Rel ( I ↾ dom 𝐴 ) ) → ( 𝐴 = ( I ↾ dom 𝐴 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ dom 𝐴 ) ) ) )
31	28 29 30	sylancl	⊢ ( 𝐴 ⊆ I → ( 𝐴 = ( I ↾ dom 𝐴 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ dom 𝐴 ) ) ) )
32	25 31	mpbird	⊢ ( 𝐴 ⊆ I → 𝐴 = ( I ↾ dom 𝐴 ) )
33		resss	⊢ ( I ↾ dom 𝐴 ) ⊆ I
34		sseq1	⊢ ( 𝐴 = ( I ↾ dom 𝐴 ) → ( 𝐴 ⊆ I ↔ ( I ↾ dom 𝐴 ) ⊆ I ) )
35	33 34	mpbiri	⊢ ( 𝐴 = ( I ↾ dom 𝐴 ) → 𝐴 ⊆ I )
36	32 35	impbii	⊢ ( 𝐴 ⊆ I ↔ 𝐴 = ( I ↾ dom 𝐴 ) )