Metamath Proof Explorer

Theorem opelco3

Description: Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018)

Ref Expression
Assertion opelco3 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) ↔ 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) )
2 relco ⊢ Rel ( 𝐶 ∘ 𝐷 )
3 2 brrelex12i ⊢ ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
5 noel ⊢ ¬ 𝐵 ∈ ∅
6 imaeq2 ⊢ ( { 𝐴 } = ∅ → ( 𝐷 “ { 𝐴 } ) = ( 𝐷 “ ∅ ) )
7 6 imaeq2d ⊢ ( { 𝐴 } = ∅ → ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) = ( 𝐶 “ ( 𝐷 “ ∅ ) ) )
8 ima0 ⊢ ( 𝐷 “ ∅ ) = ∅
9 8 imaeq2i ⊢ ( 𝐶 “ ( 𝐷 “ ∅ ) ) = ( 𝐶 “ ∅ )
10 ima0 ⊢ ( 𝐶 “ ∅ ) = ∅
11 9 10 eqtri ⊢ ( 𝐶 “ ( 𝐷 “ ∅ ) ) = ∅
12 7 11 eqtrdi ⊢ ( { 𝐴 } = ∅ → ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) = ∅ )
13 12 eleq2d ⊢ ( { 𝐴 } = ∅ → ( 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) ↔ 𝐵 ∈ ∅ ) )
14 5 13 mtbiri ⊢ ( { 𝐴 } = ∅ → ¬ 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) )
15 4 14 sylbi ⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) )
16 15 con4i ⊢ ( 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) → 𝐴 ∈ V )
17 elex ⊢ ( 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) → 𝐵 ∈ V )
18 16 17 jca ⊢ ( 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
19 df-rex ⊢ ( ∃ 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) 𝑧 𝐶 𝐵 ↔ ∃ 𝑧 ( 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) ∧ 𝑧 𝐶 𝐵 ) )
20 elimasng ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐷 ) )
21 20 elvd ⊢ ( 𝐴 ∈ V → ( 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐷 ) )
22 df-br ⊢ ( 𝐴 𝐷 𝑧 ↔ ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐷 )
23 21 22 bitr4di ⊢ ( 𝐴 ∈ V → ( 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) ↔ 𝐴 𝐷 𝑧 ) )
24 23 adantr ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) ↔ 𝐴 𝐷 𝑧 ) )
25 24 anbi1d ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) ∧ 𝑧 𝐶 𝐵 ) ↔ ( 𝐴 𝐷 𝑧 ∧ 𝑧 𝐶 𝐵 ) ) )
26 25 exbidv ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∃ 𝑧 ( 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) ∧ 𝑧 𝐶 𝐵 ) ↔ ∃ 𝑧 ( 𝐴 𝐷 𝑧 ∧ 𝑧 𝐶 𝐵 ) ) )
27 19 26 syl5rbb ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∃ 𝑧 ( 𝐴 𝐷 𝑧 ∧ 𝑧 𝐶 𝐵 ) ↔ ∃ 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) 𝑧 𝐶 𝐵 ) )
28 brcog ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑧 ( 𝐴 𝐷 𝑧 ∧ 𝑧 𝐶 𝐵 ) ) )
29 elimag ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) ↔ ∃ 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) 𝑧 𝐶 𝐵 ) )
30 29 adantl ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) ↔ ∃ 𝑧 ∈ ( 𝐷 “ { 𝐴 } ) 𝑧 𝐶 𝐵 ) )
31 27 28 30 3bitr4d ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) ) )
32 3 18 31 pm5.21nii ⊢ ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) )
33 1 32 bitr3i ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) ↔ 𝐵 ∈ ( 𝐶 “ ( 𝐷 “ { 𝐴 } ) ) )