cgraer

Description: The angle congruence relation is an equivalence relation. (Contributed by Thierry Arnoux, 31-Aug-2026)

	Ref	Expression
Hypotheses	cgraer.p	$⊢ P = {Base}_{G}$
	cgraer.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	cgraer.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	cgraer.g	$⊢ φ \to G \in 𝒢_{Tarski}$
Assertion	cgraer	$⊢ φ \to (\underset{˙}{\sim} \cap (A \times A)) Er A$

Proof

Step	Hyp	Ref	Expression
1		cgraer.p	$⊢ P = {Base}_{G}$
2		cgraer.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		cgraer.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
4		cgraer.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		relinxp	$⊢ Rel (\underset{˙}{\sim} \cap (A \times A))$
6	5	a1i	$⊢ φ \to Rel (\underset{˙}{\sim} \cap (A \times A))$
7		brinxp2	$⊢ e (\underset{˙}{\sim} \cap (A \times A)) f \leftrightarrow ((e \in A \land f \in A) \land e \underset{˙}{\sim} f)$
8	7	bilani	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \to ((e \in A \land f \in A) \land e \underset{˙}{\sim} f)$
9	8	simplrd	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \to f \in A$
10	8	simplld	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \to e \in A$
11	3	a1i	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
12	11	eqcomd	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
13		eqid	$⊢ Itv (G) = Itv (G)$
14	4	ad7antr	$⊢ (((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to G \in 𝒢_{Tarski}$
15	14	ad6antr	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to G \in 𝒢_{Tarski}$
16		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
17		simp-6r	$⊢ (((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to x \in P$
18	17	ad6antr	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to x \in P$
19		simp-11r	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to y \in P$
20		simp-10r	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to z \in P$
21		simp-6r	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to u \in P$
22		simp-5r	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to v \in P$
23		simp-4r	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to w \in P$
24	8	simprd	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \to e \underset{˙}{\sim} f$
25	24	ad6antr	$⊢ (((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to e \underset{˙}{\sim} f$
26	25	ad6antr	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to e \underset{˙}{\sim} f$
27	11 26	breqdi	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to e \sim_{𝒢}^{∠} (G) f$
28		simp-9r	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to e = ⟨“ x y z ”⟩$
29		simpllr	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to f = ⟨“ u v w ”⟩$
30	27 28 29	3brtr3d	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to ⟨“ x y z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ u v w ”⟩$
31	1 13 15 16 18 19 20 21 22 23 30	cgracom	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to ⟨“ u v w ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ x y z ”⟩$
32	12 31	breqdi	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to ⟨“ u v w ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩$
33	32 29 28	3brtr4d	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to f \underset{˙}{\sim} e$
34	33	anasss	$⊢ ((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land (u \neq v \land v \neq w)) \to f \underset{˙}{\sim} e$
35	34	anasss	$⊢ (((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to f \underset{˙}{\sim} e$
36	35	r19.29an	$⊢ ((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land \exists w \in P (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to f \underset{˙}{\sim} e$
37	1	fvexi	$⊢ P \in V$
38	9	ad6antr	$⊢ (((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to f \in A$
39	37 2 38	elcgrabasi	$⊢ (((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to \exists u \in P \exists v \in P \exists w \in P (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))$
40	36 39	r19.29vva	$⊢ (((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to f \underset{˙}{\sim} e$
41	40	anasss	$⊢ ((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land (x \neq y \land y \neq z)) \to f \underset{˙}{\sim} e$
42	41	anasss	$⊢ (((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land z \in P) \land (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to f \underset{˙}{\sim} e$
43	42	r19.29an	$⊢ ((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land x \in P) \land y \in P) \land \exists z \in P (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to f \underset{˙}{\sim} e$
44	37 2 10	elcgrabasi	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \to \exists x \in P \exists y \in P \exists z \in P (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))$
45	43 44	r19.29vva	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \to f \underset{˙}{\sim} e$
46		brinxp2	$⊢ f (\underset{˙}{\sim} \cap (A \times A)) e \leftrightarrow ((f \in A \land e \in A) \land f \underset{˙}{\sim} e)$
47	9 10 45 46	syl21anbrc	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \to f (\underset{˙}{\sim} \cap (A \times A)) e$
48	10	adantr	$⊢ ((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \to e \in A$
49	48	ad6antr	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to e \in A$
50	49	ad6antr	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to e \in A$
51	50	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to e \in A$
52		brinxp2	$⊢ f (\underset{˙}{\sim} \cap (A \times A)) g \leftrightarrow ((f \in A \land g \in A) \land f \underset{˙}{\sim} g)$
53	52	biimpi	$⊢ f (\underset{˙}{\sim} \cap (A \times A)) g \to ((f \in A \land g \in A) \land f \underset{˙}{\sim} g)$
54	53	simplrd	$⊢ f (\underset{˙}{\sim} \cap (A \times A)) g \to g \in A$
55	54	ad7antlr	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to g \in A$
56	55	ad6antr	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to g \in A$
57	56	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to g \in A$
58	3	eqcomi	$⊢ \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
59	58	a1i	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
60	4	ad8antr	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to G \in 𝒢_{Tarski}$
61	60	ad6antr	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to G \in 𝒢_{Tarski}$
62	61	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to G \in 𝒢_{Tarski}$
63		simp-6r	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to x \in P$
64	63	ad6antr	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to x \in P$
65	64	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to x \in P$
66		simp-11r	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to y \in P$
67	66	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to y \in P$
68		simp-10r	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to z \in P$
69	68	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to z \in P$
70		simp-6r	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to u \in P$
71	70	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to u \in P$
72		simp-11r	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to v \in P$
73		simp-10r	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to w \in P$
74	3	a1i	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
75	24	ad7antr	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to e \underset{˙}{\sim} f$
76	75	ad6antr	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to e \underset{˙}{\sim} f$
77	76	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to e \underset{˙}{\sim} f$
78	74 77	breqdi	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to e \sim_{𝒢}^{∠} (G) f$
79		simp-9r	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to e = ⟨“ x y z ”⟩$
80	79	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to e = ⟨“ x y z ”⟩$
81		simp-9r	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to f = ⟨“ u v w ”⟩$
82	78 80 81	3brtr3d	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to ⟨“ x y z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ u v w ”⟩$
83		simp-6r	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to i \in P$
84		simp-5r	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to j \in P$
85		simp-4r	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to k \in P$
86	53	simprd	$⊢ f (\underset{˙}{\sim} \cap (A \times A)) g \to f \underset{˙}{\sim} g$
87	86	ad7antlr	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to f \underset{˙}{\sim} g$
88	87	ad6antr	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to f \underset{˙}{\sim} g$
89	88	ad6antr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to f \underset{˙}{\sim} g$
90	74 89	breqdi	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to f \sim_{𝒢}^{∠} (G) g$
91		simpllr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to g = ⟨“ i j k ”⟩$
92	90 81 91	3brtr3d	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to ⟨“ u v w ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ i j k ”⟩$
93	1 13 62 16 65 67 69 71 72 73 82 83 84 85 92	cgratr	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to ⟨“ x y z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ i j k ”⟩$
94	59 93	breqdi	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to ⟨“ x y z ”⟩ \underset{˙}{\sim} ⟨“ i j k ”⟩$
95	94 80 91	3brtr4d	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to e \underset{˙}{\sim} g$
96		brinxp2	$⊢ e (\underset{˙}{\sim} \cap (A \times A)) g \leftrightarrow ((e \in A \land g \in A) \land e \underset{˙}{\sim} g)$
97	51 57 95 96	syl21anbrc	$⊢ ((((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land i \neq j) \land j \neq k) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
98	97	anasss	$⊢ (((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land g = ⟨“ i j k ”⟩) \land (i \neq j \land j \neq k)) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
99	98	anasss	$⊢ ((((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land k \in P) \land (g = ⟨“ i j k ”⟩ \land (i \neq j \land j \neq k))) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
100	99	r19.29an	$⊢ (((((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land i \in P) \land j \in P) \land \exists k \in P (g = ⟨“ i j k ”⟩ \land (i \neq j \land j \neq k))) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
101	37 2 56	elcgrabasi	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to \exists i \in P \exists j \in P \exists k \in P (g = ⟨“ i j k ”⟩ \land (i \neq j \land j \neq k))$
102	100 101	r19.29vva	$⊢ ((((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
103	102	anasss	$⊢ (((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \land (u \neq v \land v \neq w)) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
104	103	anasss	$⊢ ((((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
105	104	r19.29an	$⊢ (((((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land \exists w \in P (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
106	39	adantl6r	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to \exists u \in P \exists v \in P \exists w \in P (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))$
107	105 106	r19.29vva	$⊢ ((((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
108	107	anasss	$⊢ (((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land (x \neq y \land y \neq z)) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
109	108	anasss	$⊢ ((((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land z \in P) \land (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
110	109	r19.29an	$⊢ (((((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \land x \in P) \land y \in P) \land \exists z \in P (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
111	37 2 48	elcgrabasi	$⊢ ((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \to \exists x \in P \exists y \in P \exists z \in P (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))$
112	110 111	r19.29vva	$⊢ ((φ \land e (\underset{˙}{\sim} \cap (A \times A)) f) \land f (\underset{˙}{\sim} \cap (A \times A)) g) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
113	112	anasss	$⊢ (φ \land (e (\underset{˙}{\sim} \cap (A \times A)) f \land f (\underset{˙}{\sim} \cap (A \times A)) g)) \to e (\underset{˙}{\sim} \cap (A \times A)) g$
114		simpr	$⊢ (φ \land e \in A) \to e \in A$
115	58	a1i	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
116	4	ad7antr	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to G \in 𝒢_{Tarski}$
117		simp-6r	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to x \in P$
118		simp-5r	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to y \in P$
119		simp-4r	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to z \in P$
120		simplr	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to x \neq y$
121		simpr	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to y \neq z$
122	1 13 116 16 117 118 119 120 121	cgraid	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to ⟨“ x y z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ x y z ”⟩$
123	115 122	breqdi	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to ⟨“ x y z ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩$
124		simpllr	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to e = ⟨“ x y z ”⟩$
125	123 124 124	3brtr4d	$⊢ (((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to e \underset{˙}{\sim} e$
126	125	anasss	$⊢ ((((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land (x \neq y \land y \neq z)) \to e \underset{˙}{\sim} e$
127	126	anasss	$⊢ (((((φ \land e \in A) \land x \in P) \land y \in P) \land z \in P) \land (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to e \underset{˙}{\sim} e$
128	127	r19.29an	$⊢ ((((φ \land e \in A) \land x \in P) \land y \in P) \land \exists z \in P (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to e \underset{˙}{\sim} e$
129	37 2 114	elcgrabasi	$⊢ (φ \land e \in A) \to \exists x \in P \exists y \in P \exists z \in P (e = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))$
130	128 129	r19.29vva	$⊢ (φ \land e \in A) \to e \underset{˙}{\sim} e$
131		brinxp2	$⊢ e (\underset{˙}{\sim} \cap (A \times A)) e \leftrightarrow ((e \in A \land e \in A) \land e \underset{˙}{\sim} e)$
132	114 114 130 131	syl21anbrc	$⊢ (φ \land e \in A) \to e (\underset{˙}{\sim} \cap (A \times A)) e$
133	131	bilani	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) e) \to ((e \in A \land e \in A) \land e \underset{˙}{\sim} e)$
134	133	simplld	$⊢ (φ \land e (\underset{˙}{\sim} \cap (A \times A)) e) \to e \in A$
135	132 134	impbida	$⊢ φ \to (e \in A \leftrightarrow e (\underset{˙}{\sim} \cap (A \times A)) e)$
136	6 47 113 135	iserd	$⊢ φ \to (\underset{˙}{\sim} \cap (A \times A)) Er A$

Metamath Proof Explorer

Theorem cgraer

Proof