Metamath Proof Explorer

Theorem dfco2

Description: Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008)

Ref Expression
Assertion dfco2 ⊢A∘B=⋃x∈VB-1x×Ax

Proof

Step Hyp Ref Expression
1 relco ⊢Rel⁡A∘B
2 reliun ⊢Rel⁡⋃x∈VB-1x×Ax↔∀x∈VRel⁡B-1x×Ax
3 relxp ⊢Rel⁡B-1x×Ax
4 3 a1i ⊢x∈V→Rel⁡B-1x×Ax
5 2 4 mprgbir ⊢Rel⁡⋃x∈VB-1x×Ax
6 opelco2g ⊢y∈V∧z∈V→yz∈A∘B↔∃xyx∈B∧xz∈A
7 6 el2v ⊢yz∈A∘B↔∃xyx∈B∧xz∈A
8 eliun ⊢yz∈⋃x∈VB-1x×Ax↔∃x∈Vyz∈B-1x×Ax
9 rexv ⊢∃x∈Vyz∈B-1x×Ax↔∃xyz∈B-1x×Ax
10 opelxp ⊢yz∈B-1x×Ax↔y∈B-1x∧z∈Ax
11 vex ⊢x∈V
12 vex ⊢y∈V
13 11 12 elimasn ⊢y∈B-1x↔xy∈B-1
14 11 12 opelcnv ⊢xy∈B-1↔yx∈B
15 13 14 bitri ⊢y∈B-1x↔yx∈B
16 vex ⊢z∈V
17 11 16 elimasn ⊢z∈Ax↔xz∈A
18 15 17 anbi12i ⊢y∈B-1x∧z∈Ax↔yx∈B∧xz∈A
19 10 18 bitri ⊢yz∈B-1x×Ax↔yx∈B∧xz∈A
20 19 exbii ⊢∃xyz∈B-1x×Ax↔∃xyx∈B∧xz∈A
21 8 9 20 3bitrri ⊢∃xyx∈B∧xz∈A↔yz∈⋃x∈VB-1x×Ax
22 7 21 bitri ⊢yz∈A∘B↔yz∈⋃x∈VB-1x×Ax
23 1 5 22 eqrelriiv ⊢A∘B=⋃x∈VB-1x×Ax