This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
15 5 14 sylcom ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
16 15 exlimdv ⊢ ( 𝐴 ⊆ I → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
17 10 16 biimtrid ⊢ ( 𝐴 ⊆ I → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
18 12 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
19 17 18 syl5ibcom ⊢ ( 𝐴 ⊆ I → ( 𝑥 = 𝑦 → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
20 9 19 biimtrid ⊢ ( 𝐴 ⊆ 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 𝐴 ) )