Theorem bj-idres

Description: Alternate expression for the restricted identity relation. The advantage of that expression is to expose it as a "bounded" class, being included in the Cartesian square of the restricting class. (Contributed by BJ, 27-Dec-2023)

This is an alternate of idinxpresid (see idinxpres ). See also elrid and elidinxp . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-idres	⊢ ( I ↾ 𝐴 ) = ( I ∩ ( 𝐴 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( I ↾ 𝐴 ) = ( I ∩ ( 𝐴 × V ) )
2		inss1	⊢ ( I ∩ ( 𝐴 × V ) ) ⊆ I
3		relinxp	⊢ Rel ( I ∩ ( 𝐴 × V ) )
4		elin	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( 𝐴 × V ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × V ) ) )
5		bj-opelidb1	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ ( 𝑥 ∈ V ∧ 𝑥 = 𝑦 ) )
6	5	simprbi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I → 𝑥 = 𝑦 )
7		opelxp1	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × V ) → 𝑥 ∈ 𝐴 )
8		simpr	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
9		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
10	9	biimpa	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
11	8 10	jca	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
12	6 7 11	syl2an	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × V ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
13	4 12	sylbi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( 𝐴 × V ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
14		opelxpi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐴 ) )
15	13 14	syl	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ∩ ( 𝐴 × V ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐴 ) )
16	3 15	relssi	⊢ ( I ∩ ( 𝐴 × V ) ) ⊆ ( 𝐴 × 𝐴 )
17	2 16	ssini	⊢ ( I ∩ ( 𝐴 × V ) ) ⊆ ( I ∩ ( 𝐴 × 𝐴 ) )
18		ssv	⊢ 𝐴 ⊆ V
19		xpss2	⊢ ( 𝐴 ⊆ V → ( 𝐴 × 𝐴 ) ⊆ ( 𝐴 × V ) )
20		sslin	⊢ ( ( 𝐴 × 𝐴 ) ⊆ ( 𝐴 × V ) → ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( I ∩ ( 𝐴 × V ) ) )
21	18 19 20	mp2b	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( I ∩ ( 𝐴 × V ) )
22	17 21	eqssi	⊢ ( I ∩ ( 𝐴 × V ) ) = ( I ∩ ( 𝐴 × 𝐴 ) )
23	1 22	eqtri	⊢ ( I ↾ 𝐴 ) = ( I ∩ ( 𝐴 × 𝐴 ) )