Metamath Proof Explorer

Theorem dfco2a

Description: Generalization of dfco2 , where C can have any value between dom A i^i ran B and _V . (Contributed by NM, 21-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dfco2a ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( 𝐴 ∘ 𝐵 ) = ∪ 𝑥 ∈ 𝐶 ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )

Proof

Step Hyp Ref Expression
1 dfco2 ⊢ ( 𝐴 ∘ 𝐵 ) = ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) )
2 vex ⊢ 𝑧 ∈ V
3 2 eliniseg ⊢ ( 𝑥 ∈ V → ( 𝑧 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ↔ 𝑧 𝐵 𝑥 ) )
4 3 elv ⊢ ( 𝑧 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ↔ 𝑧 𝐵 𝑥 )
5 vex ⊢ 𝑥 ∈ V
6 2 5 brelrn ⊢ ( 𝑧 𝐵 𝑥 → 𝑥 ∈ ran 𝐵 )
7 4 6 sylbi ⊢ ( 𝑧 ∈ ( ◡ 𝐵 “ { 𝑥 } ) → 𝑥 ∈ ran 𝐵 )
8 vex ⊢ 𝑤 ∈ V
9 5 8 elimasn ⊢ ( 𝑤 ∈ ( 𝐴 “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑤 ⟩ ∈ 𝐴 )
10 5 8 opeldm ⊢ ( ⟨ 𝑥 , 𝑤 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 )
11 9 10 sylbi ⊢ ( 𝑤 ∈ ( 𝐴 “ { 𝑥 } ) → 𝑥 ∈ dom 𝐴 )
12 7 11 anim12ci ⊢ ( ( 𝑧 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ∧ 𝑤 ∈ ( 𝐴 “ { 𝑥 } ) ) → ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ ran 𝐵 ) )
13 12 adantl ⊢ ( ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ( 𝑧 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ∧ 𝑤 ∈ ( 𝐴 “ { 𝑥 } ) ) ) → ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ ran 𝐵 ) )
14 13 exlimivv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ( 𝑧 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ∧ 𝑤 ∈ ( 𝐴 “ { 𝑥 } ) ) ) → ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ ran 𝐵 ) )
15 elxp ⊢ ( 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ( 𝑧 ∈ ( ◡ 𝐵 “ { 𝑥 } ) ∧ 𝑤 ∈ ( 𝐴 “ { 𝑥 } ) ) ) )
16 elin ⊢ ( 𝑥 ∈ ( dom 𝐴 ∩ ran 𝐵 ) ↔ ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ ran 𝐵 ) )
17 14 15 16 3imtr4i ⊢ ( 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) → 𝑥 ∈ ( dom 𝐴 ∩ ran 𝐵 ) )
18 ssel ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( 𝑥 ∈ ( dom 𝐴 ∩ ran 𝐵 ) → 𝑥 ∈ 𝐶 ) )
19 17 18 syl5 ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) → 𝑥 ∈ 𝐶 ) )
20 19 pm4.71rd ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ) ) )
21 20 exbidv ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( ∃ 𝑥 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ) ) )
22 rexv ⊢ ( ∃ 𝑥 ∈ V 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
23 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ) )
24 21 22 23 3bitr4g ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( ∃ 𝑥 ∈ V 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ) )
25 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ∈ V 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
26 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐶 ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
27 24 25 26 3bitr4g ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( 𝑦 ∈ ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐶 ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) ) )
28 27 eqrdv ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ∪ 𝑥 ∈ V ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) = ∪ 𝑥 ∈ 𝐶 ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )
29 1 28 syl5eq ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( 𝐴 ∘ 𝐵 ) = ∪ 𝑥 ∈ 𝐶 ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )