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