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 ⊢ A B ∈ C ∘ D ↔ B ∈ C D A

Proof

Step Hyp Ref Expression
1 df-br ⊢ A C ∘ D B ↔ A B ∈ C ∘ D
2 relco ⊢ Rel ⁡ C ∘ D
3 2 brrelex12i ⊢ A C ∘ D B → A ∈ V ∧ B ∈ V
4 snprc ⊢ ¬ A ∈ V ↔ A = ∅
5 noel ⊢ ¬ B ∈ ∅
6 imaeq2 ⊢ A = ∅ → D A = D ∅
7 6 imaeq2d ⊢ A = ∅ → C D A = C D ∅
8 ima0 ⊢ D ∅ = ∅
9 8 imaeq2i ⊢ C D ∅ = C ∅
10 ima0 ⊢ C ∅ = ∅
11 9 10 eqtri ⊢ C D ∅ = ∅
12 7 11 syl6eq ⊢ A = ∅ → C D A = ∅
13 12 eleq2d ⊢ A = ∅ → B ∈ C D A ↔ B ∈ ∅
14 5 13 mtbiri ⊢ A = ∅ → ¬ B ∈ C D A
15 4 14 sylbi ⊢ ¬ A ∈ V → ¬ B ∈ C D A
16 15 con4i ⊢ B ∈ C D A → A ∈ V
17 elex ⊢ B ∈ C D A → B ∈ V
18 16 17 jca ⊢ B ∈ C D A → A ∈ V ∧ B ∈ V
19 df-rex ⊢ ∃ z ∈ D A z C B ↔ ∃ z z ∈ D A ∧ z C B
20 elimasng ⊢ A ∈ V ∧ z ∈ V → z ∈ D A ↔ A z ∈ D
21 20 elvd ⊢ A ∈ V → z ∈ D A ↔ A z ∈ D
22 df-br ⊢ A D z ↔ A z ∈ D
23 21 22 syl6bbr ⊢ A ∈ V → z ∈ D A ↔ A D z
24 23 adantr ⊢ A ∈ V ∧ B ∈ V → z ∈ D A ↔ A D z
25 24 anbi1d ⊢ A ∈ V ∧ B ∈ V → z ∈ D A ∧ z C B ↔ A D z ∧ z C B
26 25 exbidv ⊢ A ∈ V ∧ B ∈ V → ∃ z z ∈ D A ∧ z C B ↔ ∃ z A D z ∧ z C B
27 19 26 syl5rbb ⊢ A ∈ V ∧ B ∈ V → ∃ z A D z ∧ z C B ↔ ∃ z ∈ D A z C B
28 brcog ⊢ A ∈ V ∧ B ∈ V → A C ∘ D B ↔ ∃ z A D z ∧ z C B
29 elimag ⊢ B ∈ V → B ∈ C D A ↔ ∃ z ∈ D A z C B
30 29 adantl ⊢ A ∈ V ∧ B ∈ V → B ∈ C D A ↔ ∃ z ∈ D A z C B
31 27 28 30 3bitr4d ⊢ A ∈ V ∧ B ∈ V → A C ∘ D B ↔ B ∈ C D A
32 3 18 31 pm5.21nii ⊢ A C ∘ D B ↔ B ∈ C D A
33 1 32 bitr3i ⊢ A B ∈ C ∘ D ↔ B ∈ C D A