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

Metamath Proof Explorer

Theorem xpidtr

Description: A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009)

Ref Expression
Assertion xpidtr ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )

Proof

Step Hyp Ref Expression
1 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
2 brxp ⊢ ( 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
3 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑧 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
4 3 simplbi2com ⊢ ( 𝑧 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 ) )
5 2 4 simplbiim ⊢ ( 𝑦 ( 𝐴 × 𝐴 ) 𝑧 → ( 𝑥 ∈ 𝐴 → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 ) )
6 5 com12 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ( 𝐴 × 𝐴 ) 𝑧 → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 ) )
7 6 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ( 𝐴 × 𝐴 ) 𝑧 → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 ) )
8 1 7 sylbi ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 → ( 𝑦 ( 𝐴 × 𝐴 ) 𝑧 → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 ) )
9 8 imp ⊢ ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 )
10 9 ax-gen ⊢ ∀ 𝑧 ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 )
11 10 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 )
12 cotr ⊢ ( ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) → 𝑥 ( 𝐴 × 𝐴 ) 𝑧 ) )
13 11 12 mpbir ⊢ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )