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

Metamath Proof Explorer

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 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )