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

Metamath Proof Explorer

Theorem iss2

Description: A subclass of the identity relation is the intersection of identity relation with Cartesian product of the domain and range of the class. (Contributed by Peter Mazsa, 22-Jul-2019)

Ref Expression
Assertion iss2 ( 𝐴 ⊆ I ↔ 𝐴 = ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 opeldm ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 )
5 1 4 jca2 ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ 𝑥 ∈ dom 𝐴 ) ) )
6 2 3 opelrn ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 ∈ ran 𝐴 )
7 1 6 jca2 ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ 𝑦 ∈ ran 𝐴 ) ) )
8 5 7 jcad ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ 𝑥 ∈ dom 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ 𝑦 ∈ ran 𝐴 ) ) ) )
9 anandi ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ 𝑥 ∈ dom 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ 𝑦 ∈ ran 𝐴 ) ) )
10 8 9 imbitrrdi ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) ) ) )
11 df-br ⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
12 3 ideq ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
13 11 12 bitr3i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑥 = 𝑦 )
14 2 eldm2 ⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
15 opeq2 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
16 15 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
17 16 biimprcd ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
18 13 17 biimtrid ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
19 1 18 sylcom ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
20 19 exlimdv ⊢ ( 𝐴 ⊆ I → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
21 14 20 biimtrid ⊢ ( 𝐴 ⊆ I → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
22 16 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
23 21 22 syl5ibcom ⊢ ( 𝐴 ⊆ I → ( 𝑥 = 𝑦 → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
24 23 imp ⊢ ( ( 𝐴 ⊆ I ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ dom 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
25 24 adantrd ⊢ ( ( 𝐴 ⊆ I ∧ 𝑥 = 𝑦 ) → ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
26 25 ex ⊢ ( 𝐴 ⊆ I → ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
27 13 26 biimtrid ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
28 27 impd ⊢ ( 𝐴 ⊆ I → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
29 10 28 impbid ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) ) ) )
30 opelinxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ↔ ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
31 30 biancomi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) ) )
32 29 31 bitr4di ⊢ ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ) )
33 32 alrimivv ⊢ ( 𝐴 ⊆ I → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ) )
34 reli ⊢ Rel I
35 relss ⊢ ( 𝐴 ⊆ I → ( Rel I → Rel 𝐴 ) )
36 34 35 mpi ⊢ ( 𝐴 ⊆ I → Rel 𝐴 )
37 relinxp ⊢ Rel ( I ∩ ( dom 𝐴 × ran 𝐴 ) )
38 eqrel ⊢ ( ( Rel 𝐴 ∧ Rel ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ) → ( 𝐴 = ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ) ) )
39 36 37 38 sylancl ⊢ ( 𝐴 ⊆ I → ( 𝐴 = ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ) ) )
40 33 39 mpbird ⊢ ( 𝐴 ⊆ I → 𝐴 = ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) )
41 inss1 ⊢ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ⊆ I
42 sseq1 ⊢ ( 𝐴 = ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) → ( 𝐴 ⊆ I ↔ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) ⊆ I ) )
43 41 42 mpbiri ⊢ ( 𝐴 = ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) → 𝐴 ⊆ I )
44 40 43 impbii ⊢ ( 𝐴 ⊆ I ↔ 𝐴 = ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) )