Theorem trcoss2 35169

Description: Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.)

Assertion

Ref	Expression
trcoss2	⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))

Distinct variable groups:   𝑦,𝑅   𝑥,𝑦   𝑦,𝑧

Allowed substitution hints:   𝑅(𝑥,𝑧)

Proof of Theorem trcoss2

Step	Hyp	Ref	Expression
1		alcom 2095	. . 3 ⊢ (∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑧∀𝑦((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
2	1	albii 1782	. 2 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧∀𝑦((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
3		19.23v 1901	. . . 4 ⊢ (∀𝑦(𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅) ↔ (∃𝑦 𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
4		eleccossin 35168	. . . . . . . 8 ⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ↔ (𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧)))
5	4	el2v 3416	. . . . . . 7 ⊢ (𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ↔ (𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧))
6	5	bicomi 216	. . . . . 6 ⊢ ((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) ↔ 𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅))
7		brcoss3 35123	. . . . . . 7 ⊢ ((𝑥 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ≀ 𝑅𝑧 ↔ ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
8	7	el2v 3416	. . . . . 6 ⊢ (𝑥 ≀ 𝑅𝑧 ↔ ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)
9	6, 8	imbi12i 343	. . . . 5 ⊢ (((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ (𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
10	9	albii 1782	. . . 4 ⊢ (∀𝑦((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑦(𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
11		n0 4190	. . . . 5 ⊢ (([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅))
12	11	imbi1i 342	. . . 4 ⊢ ((([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅) ↔ (∃𝑦 𝑦 ∈ ([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
13	3, 10, 12	3bitr4i 295	. . 3 ⊢ (∀𝑦((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ (([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
14	13	2albii 1783	. 2 ⊢ (∀𝑥∀𝑧∀𝑦((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
15	2, 14	bitri 267	1 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387  ∀wal 1505  ∃wex 1742   ∈ wcel 2050   ≠ wne 2961  Vcvv 3409   ∩ cin 3822  ∅c0 4172   class class class wbr 4923  ^◡ccnv 5400  [cec 8081   ≀ ccoss 34897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-opab 4986  df-xp 5407  df-rel 5408  df-cnv 5409  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-ec 8085  df-coss 35104

This theorem is referenced by:  eqvrelcoss4  35300