Theorem idinxpssinxp2

Description: Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 4-Mar-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	idinxpssinxp2	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		idinxpresid	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ↾ 𝐴 )
2	1	sseq1i	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ( I ↾ 𝐴 ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
3		idrefALT	⊢ ( ( I ↾ 𝐴 ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 )
4		brinxp2	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝑥 ) )
5		pm4.24	⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
6	5	anbi1i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝑥 ) )
7	4 6	bitr4i	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑥 ) )
8	7	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑥 ) )
9	2 3 8	3bitri	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑥 ) )
10		ralanid	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )
11	9 10	bitri	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )