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 ( ( ◡ 𝐵 “ { 𝑥 } ) × ( 𝐴 “ { 𝑥 } ) )