Theorem xptrrel 13567

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

Assertion

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

Proof of Theorem xptrrel

Step	Hyp	Ref	Expression
1		inss1 3795	. . . . . . . 8 ⊢ (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) ⊆ dom (𝐴 × 𝐵)
2		dmxpss 5484	. . . . . . . 8 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
3	1, 2	sstri 3577	. . . . . . 7 ⊢ (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) ⊆ 𝐴
4		inss2 3796	. . . . . . . 8 ⊢ (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) ⊆ ran (𝐴 × 𝐵)
5		rnxpss 5485	. . . . . . . 8 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
6	4, 5	sstri 3577	. . . . . . 7 ⊢ (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) ⊆ 𝐵
7	3, 6	ssini 3798	. . . . . 6 ⊢ (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) ⊆ (𝐴 ∩ 𝐵)
8		eqimss 3620	. . . . . 6 ⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∩ 𝐵) ⊆ ∅)
9	7, 8	syl5ss 3579	. . . . 5 ⊢ ((𝐴 ∩ 𝐵) = ∅ → (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) ⊆ ∅)
10		ss0 3926	. . . . 5 ⊢ ((dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) ⊆ ∅ → (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) = ∅)
11	9, 10	syl 17	. . . 4 ⊢ ((𝐴 ∩ 𝐵) = ∅ → (dom (𝐴 × 𝐵) ∩ ran (𝐴 × 𝐵)) = ∅)
12	11	coemptyd 13566	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) = ∅)
13		0ss 3924	. . 3 ⊢ ∅ ⊆ (𝐴 × 𝐵)
14	12, 13	syl6eqss 3618	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵))
15		df-ne 2782	. . . . 5 ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ¬ (𝐴 ∩ 𝐵) = ∅)
16	15	biimpri 217	. . . 4 ⊢ (¬ (𝐴 ∩ 𝐵) = ∅ → (𝐴 ∩ 𝐵) ≠ ∅)
17	16	xpcoidgend 13562	. . 3 ⊢ (¬ (𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐵))
18		ssid 3587	. . 3 ⊢ (𝐴 × 𝐵) ⊆ (𝐴 × 𝐵)
19	17, 18	syl6eqss 3618	. 2 ⊢ (¬ (𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵))
20	14, 19	pm2.61i 175	1 ⊢ ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)

Syntax hints:  ¬ wn 3   = wceq 1475   ≠ wne 2780   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874   × cxp 5036  dom cdm 5038  ran crn 5039   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050

This theorem is referenced by:  trclublem  13582  trclubgNEW  36944  trclexi  36946  cnvtrcl0  36952  xpintrreld  36977  trrelsuperreldg  36979  trrelsuperrel2dg  36982