Metamath Proof Explorer


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