Theorem cotrgOLD 6127

Description: Obsolete version of cotrg 6126 as of 29-Dec-2024. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6129. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
cotrgOLD	⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧

Proof of Theorem cotrgOLD

Step	Hyp	Ref	Expression
1		relco 6125	. . 3 ⊢ Rel (𝐴 ∘ 𝐵)
2		ssrel3 5795	. . 3 ⊢ (Rel (𝐴 ∘ 𝐵) → ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑧(𝑥(𝐴 ∘ 𝐵)𝑧 → 𝑥𝐶𝑧)))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑧(𝑥(𝐴 ∘ 𝐵)𝑧 → 𝑥𝐶𝑧))
4		vex 3483	. . . . . . . 8 ⊢ 𝑥 ∈ V
5		vex 3483	. . . . . . . 8 ⊢ 𝑧 ∈ V
6	4, 5	brco 5880	. . . . . . 7 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑧 ↔ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
7	6	imbi1i 349	. . . . . 6 ⊢ ((𝑥(𝐴 ∘ 𝐵)𝑧 → 𝑥𝐶𝑧) ↔ (∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
8		19.23v 1941	. . . . . 6 ⊢ (∀𝑦((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
9	7, 8	bitr4i 278	. . . . 5 ⊢ ((𝑥(𝐴 ∘ 𝐵)𝑧 → 𝑥𝐶𝑧) ↔ ∀𝑦((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
10	9	albii 1818	. . . 4 ⊢ (∀𝑧(𝑥(𝐴 ∘ 𝐵)𝑧 → 𝑥𝐶𝑧) ↔ ∀𝑧∀𝑦((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
11		alcom 2158	. . . 4 ⊢ (∀𝑧∀𝑦((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
12	10, 11	bitri 275	. . 3 ⊢ (∀𝑧(𝑥(𝐴 ∘ 𝐵)𝑧 → 𝑥𝐶𝑧) ↔ ∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
13	12	albii 1818	. 2 ⊢ (∀𝑥∀𝑧(𝑥(𝐴 ∘ 𝐵)𝑧 → 𝑥𝐶𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
14	3, 13	bitri 275	1 ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537  ∃wex 1778   ⊆ wss 3950   class class class wbr 5142   ∘ ccom 5688  Rel wrel 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-11 2156  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-xp 5690  df-rel 5691  df-co 5693

This theorem is referenced by: (None)