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