Theorem opelco3 33131

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

Assertion

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

Proof of Theorem opelco3

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-br 5031	. 2 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷))
2		relco 6064	. . . 4 ⊢ Rel (𝐶 ∘ 𝐷)
3	2	brrelex12i 5571	. . 3 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
4		snprc 4613	. . . . . 6 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
5		noel 4247	. . . . . . 7 ⊢ ¬ 𝐵 ∈ ∅
6		imaeq2 5892	. . . . . . . . . 10 ⊢ ({𝐴} = ∅ → (𝐷 “ {𝐴}) = (𝐷 “ ∅))
7	6	imaeq2d 5896	. . . . . . . . 9 ⊢ ({𝐴} = ∅ → (𝐶 “ (𝐷 “ {𝐴})) = (𝐶 “ (𝐷 “ ∅)))
8		ima0 5912	. . . . . . . . . . 11 ⊢ (𝐷 “ ∅) = ∅
9	8	imaeq2i 5894	. . . . . . . . . 10 ⊢ (𝐶 “ (𝐷 “ ∅)) = (𝐶 “ ∅)
10		ima0 5912	. . . . . . . . . 10 ⊢ (𝐶 “ ∅) = ∅
11	9, 10	eqtri 2821	. . . . . . . . 9 ⊢ (𝐶 “ (𝐷 “ ∅)) = ∅
12	7, 11	eqtrdi 2849	. . . . . . . 8 ⊢ ({𝐴} = ∅ → (𝐶 “ (𝐷 “ {𝐴})) = ∅)
13	12	eleq2d 2875	. . . . . . 7 ⊢ ({𝐴} = ∅ → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ 𝐵 ∈ ∅))
14	5, 13	mtbiri 330	. . . . . 6 ⊢ ({𝐴} = ∅ → ¬ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
15	4, 14	sylbi 220	. . . . 5 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
16	15	con4i 114	. . . 4 ⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → 𝐴 ∈ V)
17		elex 3459	. . . 4 ⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → 𝐵 ∈ V)
18	16, 17	jca 515	. . 3 ⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
19		df-rex 3112	. . . . 5 ⊢ (∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵 ↔ ∃𝑧(𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵))
20		elimasng 5922	. . . . . . . . . 10 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ V) → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ ⟨𝐴, 𝑧⟩ ∈ 𝐷))
21	20	elvd 3447	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ ⟨𝐴, 𝑧⟩ ∈ 𝐷))
22		df-br 5031	. . . . . . . . 9 ⊢ (𝐴𝐷𝑧 ↔ ⟨𝐴, 𝑧⟩ ∈ 𝐷)
23	21, 22	syl6bbr 292	. . . . . . . 8 ⊢ (𝐴 ∈ V → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 𝐴𝐷𝑧))
24	23	adantr 484	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 𝐴𝐷𝑧))
25	24	anbi1d 632	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵) ↔ (𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵)))
26	25	exbidv 1922	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∃𝑧(𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵) ↔ ∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵)))
27	19, 26	syl5rbb 287	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵))
28		brcog 5701	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵)))
29		elimag 5900	. . . . 5 ⊢ (𝐵 ∈ V → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵))
30	29	adantl 485	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵))
31	27, 28, 30	3bitr4d 314	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))))
32	3, 18, 31	pm5.21nii 383	. 2 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
33	1, 32	bitr3i 280	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107  Vcvv 3441  ∅c0 4243  {csn 4525  ⟨cop 4531   class class class wbr 5030   “ cima 5522   ∘ ccom 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by: (None)