Theorem xpcogend

Description: The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypothesis	xpcogend.1	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )
Assertion	xpcogend	⊢ ( 𝜑 → ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		xpcogend.1	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )
2		brxp	⊢ ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3		brxp	⊢ ( 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) )
4	3	biancomi	⊢ ( 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ↔ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) )
5	2 4	anbi12i	⊢ ( ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) )
6	5	exbii	⊢ ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) )
7		an4	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
8	7	exbii	⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
9		19.42v	⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
10	6 8 9	3bitri	⊢ ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
11		ndisj	⊢ ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
12	1 11	sylib	⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
13	12	biantrud	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
14	10 13	bitr4id	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ) )
15	14	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) } )
16		df-co	⊢ ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) }
17		df-xp	⊢ ( 𝐴 × 𝐷 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) }
18	15 16 17	3eqtr4g	⊢ ( 𝜑 → ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐷 ) )