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	⊢ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )