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

Metamath Proof Explorer

Theorem xptrrel

Description: The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion xptrrel ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 )

Proof

Step Hyp Ref Expression
1 inss1 ⊢ ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) ⊆ dom ( 𝐴 × 𝐵 )
2 dmxpss ⊢ dom ( 𝐴 × 𝐵 ) ⊆ 𝐴
3 1 2 sstri ⊢ ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) ⊆ 𝐴
4 inss2 ⊢ ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) ⊆ ran ( 𝐴 × 𝐵 )
5 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
6 4 5 sstri ⊢ ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) ⊆ 𝐵
7 3 6 ssini ⊢ ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 )
8 eqimss ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ 𝐵 ) ⊆ ∅ )
9 7 8 sstrid ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) ⊆ ∅ )
10 ss0 ⊢ ( ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) ⊆ ∅ → ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) = ∅ )
11 9 10 syl ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( dom ( 𝐴 × 𝐵 ) ∩ ran ( 𝐴 × 𝐵 ) ) = ∅ )
12 11 coemptyd ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) = ∅ )
13 0ss ⊢ ∅ ⊆ ( 𝐴 × 𝐵 )
14 12 13 eqsstrdi ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 ) )
15 neqne ⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
16 15 xpcoidgend ⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐵 ) )
17 ssid ⊢ ( 𝐴 × 𝐵 ) ⊆ ( 𝐴 × 𝐵 )
18 16 17 eqsstrdi ⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 ) )
19 14 18 pm2.61i ⊢ ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 )