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	eqtrid	⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ 𝐶 → ( 𝐴 ∘ 𝐵 ) = ∪ 𝑥 ∈ 𝐶 ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) ) )