Metamath Proof Explorer

Theorem xpco2

Description: Composition of a Cartesian product with a function. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Assertion xpco2 ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐵 × 𝐶 ) ∘ 𝐹 ) = ( 𝐴 × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ( ( 𝐵 × 𝐶 ) ∘ 𝐹 )
2 relxp ⊢ Rel ( 𝐴 × 𝐶 )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑧 ∈ V
5 3 4 breldm ⊢ ( 𝑥 𝐹 𝑧 → 𝑥 ∈ dom 𝐹 )
6 5 ad2antrl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ) → 𝑥 ∈ dom 𝐹 )
7 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
8 7 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ) → dom 𝐹 = 𝐴 )
9 6 8 eleqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ) → 𝑥 ∈ 𝐴 )
10 brxp ⊢ ( 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
11 10 simprbi ⊢ ( 𝑧 ( 𝐵 × 𝐶 ) 𝑦 → 𝑦 ∈ 𝐶 )
12 11 ad2antll ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ) → 𝑦 ∈ 𝐶 )
13 9 12 jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) )
14 13 ex ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
15 14 exlimdv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑧 ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
16 15 imp ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑧 ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) )
17 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
18 17 adantrr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
19 ffvbr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) )
20 19 adantrr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) )
21 simprr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
22 brxp ⊢ ( ( 𝐹 ‘ 𝑥 ) ( 𝐵 × 𝐶 ) 𝑦 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
23 18 21 22 sylanbrc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑥 ) ( 𝐵 × 𝐶 ) 𝑦 )
24 20 23 jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ∧ ( 𝐹 ‘ 𝑥 ) ( 𝐵 × 𝐶 ) 𝑦 ) )
25 breq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑥 𝐹 𝑧 ↔ 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ) )
26 breq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ( 𝐵 × 𝐶 ) 𝑦 ) )
27 25 26 anbi12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ↔ ( 𝑥 𝐹 ( 𝐹 ‘ 𝑥 ) ∧ ( 𝐹 ‘ 𝑥 ) ( 𝐵 × 𝐶 ) 𝑦 ) ) )
28 18 24 27 spcedv ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ∃ 𝑧 ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) )
29 16 28 impbida ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑧 ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) )
30 vex ⊢ 𝑦 ∈ V
31 3 30 brco ⊢ ( 𝑥 ( ( 𝐵 × 𝐶 ) ∘ 𝐹 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( 𝐵 × 𝐶 ) 𝑦 ) )
32 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐶 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) )
33 29 31 32 3bitr4g ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 ( ( 𝐵 × 𝐶 ) ∘ 𝐹 ) 𝑦 ↔ 𝑥 ( 𝐴 × 𝐶 ) 𝑦 ) )
34 1 2 33 eqbrrdiv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐵 × 𝐶 ) ∘ 𝐹 ) = ( 𝐴 × 𝐶 ) )