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 syl6ibr ( 𝐴 ⊆ 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 syl5bi ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
19 1 18 sylcom ( 𝐴 ⊆ I → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
20 19 exlimdv ( 𝐴 ⊆ I → ( ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝐴 ) )
21 14 20 syl5bi ( 𝐴 ⊆ 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 syl5bi ( 𝐴 ⊆ 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 𝐴 ) ) )