Metamath Proof Explorer

Definition df-cgr3

Description: The three place congruence predicate. This is an abbreviation for saying that all three pair in a triple are congruent with each other. Three place form of Definition 4.4 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion df-cgr3 ${⊢}\mathrm{Cgr3}=\left\{⟨{p},{q}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {a}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)\right\}$

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccgr3 ${class}\mathrm{Cgr3}$
1 vp ${setvar}{p}$
2 vq ${setvar}{q}$
3 vn ${setvar}{n}$
4 cn ${class}ℕ$
5 va ${setvar}{a}$
6 cee ${class}𝔼$
7 3 cv ${setvar}{n}$
8 7 6 cfv ${class}𝔼\left({n}\right)$
9 vb ${setvar}{b}$
10 vc ${setvar}{c}$
11 vd ${setvar}{d}$
12 ve ${setvar}{e}$
13 vf ${setvar}{f}$
14 1 cv ${setvar}{p}$
15 5 cv ${setvar}{a}$
16 9 cv ${setvar}{b}$
17 10 cv ${setvar}{c}$
18 16 17 cop ${class}⟨{b},{c}⟩$
19 15 18 cop ${class}⟨{a},⟨{b},{c}⟩⟩$
20 14 19 wceq ${wff}{p}=⟨{a},⟨{b},{c}⟩⟩$
21 2 cv ${setvar}{q}$
22 11 cv ${setvar}{d}$
23 12 cv ${setvar}{e}$
24 13 cv ${setvar}{f}$
25 23 24 cop ${class}⟨{e},{f}⟩$
26 22 25 cop ${class}⟨{d},⟨{e},{f}⟩⟩$
27 21 26 wceq ${wff}{q}=⟨{d},⟨{e},{f}⟩⟩$
28 15 16 cop ${class}⟨{a},{b}⟩$
29 ccgr ${class}\mathrm{Cgr}$
30 22 23 cop ${class}⟨{d},{e}⟩$
31 28 30 29 wbr ${wff}⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩$
32 15 17 cop ${class}⟨{a},{c}⟩$
33 22 24 cop ${class}⟨{d},{f}⟩$
34 32 33 29 wbr ${wff}⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩$
35 18 25 29 wbr ${wff}⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩$
36 31 34 35 w3a ${wff}\left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)$
37 20 27 36 w3a ${wff}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
38 37 13 8 wrex ${wff}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
39 38 12 8 wrex ${wff}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
40 39 11 8 wrex ${wff}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
41 40 10 8 wrex ${wff}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
42 41 9 8 wrex ${wff}\exists {b}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
43 42 5 8 wrex ${wff}\exists {a}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
44 43 3 4 wrex ${wff}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {a}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
45 44 1 2 copab ${class}\left\{⟨{p},{q}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {a}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)\right\}$
46 0 45 wceq ${wff}\mathrm{Cgr3}=\left\{⟨{p},{q}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {a}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)\right\}$