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 ∈ V B -1 x × A x

Proof

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