This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∘ 𝐵 ) = ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ( 𝐴 ∘ 𝐵 )
2 reliun ⊢ ( Rel ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ V Rel ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
3 relxp ⊢ Rel ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) )
4 3 a1i ⊢ ( 𝑥 ∈ V → Rel ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
5 2 4 mprgbir ⊢ Rel ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) )
6 opelco2g ⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐴 ) ) )
7 6 el2v ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐴 ) )
8 eliun ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ∈ V ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
9 rexv ⊢ ( ∃ 𝑥 ∈ V ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
10 opelxp ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ( 𝑦 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑥 } ) ) )
11 vex ⊢ 𝑥 ∈ V
12 vex ⊢ 𝑦 ∈ V
13 11 12 elimasn ⊢ ( 𝑦 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐵 )
14 11 12 opelcnv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐵 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 )
15 13 14 bitri ⊢ ( 𝑦 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 )
16 vex ⊢ 𝑧 ∈ V
17 11 16 elimasn ⊢ ( 𝑧 ∈ ( 𝐴 “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐴 )
18 15 17 anbi12i ⊢ ( ( 𝑦 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑥 } ) ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐴 ) )
19 10 18 bitri ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐴 ) )
20 19 exbii ⊢ ( ∃ 𝑥 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐴 ) )
21 8 9 20 3bitrri ⊢ ( ∃ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐴 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
22 7 21 bitri ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
23 1 5 22 eqrelriiv ⊢ ( 𝐴 ∘ 𝐵 ) = ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) )