iscgra

Description: Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of Schwabhauser p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020)

	Ref	Expression
Hypotheses	iscgra.p	$⊢ P = {Base}_{G}$
	iscgra.i	$⊢ I = Itv (G)$
	iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
	iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iscgra.a	$⊢ φ \to A \in P$
	iscgra.b	$⊢ φ \to B \in P$
	iscgra.c	$⊢ φ \to C \in P$
	iscgra.d	$⊢ φ \to D \in P$
	iscgra.e	$⊢ φ \to E \in P$
	iscgra.f	$⊢ φ \to F \in P$
Assertion	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$

Proof

Step	Hyp	Ref	Expression
1		iscgra.p	$⊢ P = {Base}_{G}$
2		iscgra.i	$⊢ I = Itv (G)$
3		iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
4		iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		iscgra.a	$⊢ φ \to A \in P$
6		iscgra.b	$⊢ φ \to B \in P$
7		iscgra.c	$⊢ φ \to C \in P$
8		iscgra.d	$⊢ φ \to D \in P$
9		iscgra.e	$⊢ φ \to E \in P$
10		iscgra.f	$⊢ φ \to F \in P$
11		simpl	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to a = ⟨“ A B C ”⟩$
12		eqidd	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to x = x$
13		simpr	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b = ⟨“ D E F ”⟩$
14	13	fveq1d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b (1) = ⟨“ D E F ”⟩ (1)$
15		eqidd	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to y = y$
16	12 14 15	s3eqd	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to ⟨“ x b (1) y ”⟩ = ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩$
17	11 16	breq12d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩)$
18	14	fveq2d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to K (b (1)) = K (⟨“ D E F ”⟩ (1))$
19	13	fveq1d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b (0) = ⟨“ D E F ”⟩ (0)$
20	12 18 19	breq123d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (x K (b (1)) b (0) \leftrightarrow x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0))$
21	13	fveq1d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to b (2) = ⟨“ D E F ”⟩ (2)$
22	15 18 21	breq123d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (y K (b (1)) b (2) \leftrightarrow y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2))$
23	17 20 22	3anbi123d	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to ((a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)))$
24	23	2rexbidv	$⊢ (a = ⟨“ A B C ”⟩ \land b = ⟨“ D E F ”⟩) \to (\exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)))$
25		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
26	24 25	brab2a	$⊢ ⟨“ A B C ”⟩ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} ⟨“ D E F ”⟩ \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)))$
27		eqidd	$⊢ (φ \land (x \in P \land y \in P)) \to x = x$
28		s3fv1	$⊢ E \in P \to ⟨“ D E F ”⟩ (1) = E$
29	9 28	syl	$⊢ φ \to ⟨“ D E F ”⟩ (1) = E$
30	29	adantr	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ D E F ”⟩ (1) = E$
31		eqidd	$⊢ (φ \land (x \in P \land y \in P)) \to y = y$
32	27 30 31	s3eqd	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ = ⟨“ x E y ”⟩$
33	32	breq2d	$⊢ (φ \land (x \in P \land y \in P)) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩)$
34	30	fveq2d	$⊢ (φ \land (x \in P \land y \in P)) \to K (⟨“ D E F ”⟩ (1)) = K (E)$
35		s3fv0	$⊢ D \in P \to ⟨“ D E F ”⟩ (0) = D$
36	8 35	syl	$⊢ φ \to ⟨“ D E F ”⟩ (0) = D$
37	36	adantr	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ D E F ”⟩ (0) = D$
38	27 34 37	breq123d	$⊢ (φ \land (x \in P \land y \in P)) \to (x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \leftrightarrow x K (E) D)$
39		s3fv2	$⊢ F \in P \to ⟨“ D E F ”⟩ (2) = F$
40	10 39	syl	$⊢ φ \to ⟨“ D E F ”⟩ (2) = F$
41	40	adantr	$⊢ (φ \land (x \in P \land y \in P)) \to ⟨“ D E F ”⟩ (2) = F$
42	31 34 41	breq123d	$⊢ (φ \land (x \in P \land y \in P)) \to (y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2) \leftrightarrow y K (E) F)$
43	33 38 42	3anbi123d	$⊢ (φ \land (x \in P \land y \in P)) \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$
44	43	2rexbidva	$⊢ φ \to (\exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2)) \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$
45	44	anbi2d	$⊢ φ \to (((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x ⟨“ D E F ”⟩ (1) y ”⟩ \land x K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (0) \land y K (⟨“ D E F ”⟩ (1)) ⟨“ D E F ”⟩ (2))) \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)))$
46	26 45	syl5bb	$⊢ φ \to (⟨“ A B C ”⟩ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} ⟨“ D E F ”⟩ \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)))$
47		elex	$⊢ G \in 𝒢_{Tarski} \to G \in V$
48		simpl	$⊢ (p = P \land k = K) \to p = P$
49	48	eqcomd	$⊢ (p = P \land k = K) \to P = p$
50	49	oveq1d	$⊢ (p = P \land k = K) \to P^{(0 ..^3)} = p^{(0 ..^3)}$
51	50	eleq2d	$⊢ (p = P \land k = K) \to (a \in (P^{(0 ..^3)}) \leftrightarrow a \in (p^{(0 ..^3)}))$
52	50	eleq2d	$⊢ (p = P \land k = K) \to (b \in (P^{(0 ..^3)}) \leftrightarrow b \in (p^{(0 ..^3)}))$
53	51 52	anbi12d	$⊢ (p = P \land k = K) \to ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \leftrightarrow (a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})))$
54		simpr	$⊢ (p = P \land k = K) \to k = K$
55	54	fveq1d	$⊢ (p = P \land k = K) \to k (b (1)) = K (b (1))$
56	55	breqd	$⊢ (p = P \land k = K) \to (x k (b (1)) b (0) \leftrightarrow x K (b (1)) b (0))$
57	55	breqd	$⊢ (p = P \land k = K) \to (y k (b (1)) b (2) \leftrightarrow y K (b (1)) b (2))$
58	56 57	3anbi23d	$⊢ (p = P \land k = K) \to ((a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)) \leftrightarrow (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
59	58	bicomd	$⊢ (p = P \land k = K) \to ((a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))$
60	49 59	rexeqbidv	$⊢ (p = P \land k = K) \to (\exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))$
61	49 60	rexeqbidv	$⊢ (p = P \land k = K) \to (\exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))$
62	53 61	anbi12d	$⊢ (p = P \land k = K) \to (((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))) \leftrightarrow ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2))))$
63	1 3 62	sbcie2s	$⊢ g = G \to (\underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2))) \leftrightarrow ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))))$
64	63	opabbidv	$⊢ g = G \to \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
65		fveq2	$⊢ g = G \to \sim_{𝒢} (g) = \sim_{𝒢} (G)$
66	65	breqd	$⊢ g = G \to (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \leftrightarrow a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩)$
67	66	3anbi1d	$⊢ g = G \to ((a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
68	67	2rexbidv	$⊢ g = G \to (\exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)) \leftrightarrow \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))$
69	68	anbi2d	$⊢ g = G \to (((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))) \leftrightarrow ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2))))$
70	69	opabbidv	$⊢ g = G \to \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
71	64 70	eqtrd	$⊢ g = G \to \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\} = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
72		df-cgra	$⊢ \sim_{𝒢}^{∠} = (g \in V ⟼ \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\})$
73		ovex	$⊢ P^{(0 ..^3)} \in V$
74	73 73	xpex	$⊢ (P^{(0 ..^3)}) \times (P^{(0 ..^3)}) \in V$
75		opabssxp	$⊢ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} \subseteq (P^{(0 ..^3)}) \times (P^{(0 ..^3)})$
76	74 75	ssexi	$⊢ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} \in V$
77	71 72 76	fvmpt	$⊢ G \in V \to \sim_{𝒢}^{∠} (G) = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
78	4 47 77	3syl	$⊢ φ \to \sim_{𝒢}^{∠} (G) = \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\}$
79	78	breqd	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \{⟨a, b⟩ \| ((a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x K (b (1)) b (0) \land y K (b (1)) b (2)))\} ⟨“ D E F ”⟩)$
80	5 6 7	s3cld	$⊢ φ \to ⟨“ A B C ”⟩ \in Word P$
81		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
82	1	fvexi	$⊢ P \in V$
83		3nn0	$⊢ 3 \in ℕ_{0}$
84		wrdmap	$⊢ (P \in V \land 3 \in ℕ_{0}) \to ((⟨“ A B C ”⟩ \in Word P \land \|⟨“ A B C ”⟩\| = 3) \leftrightarrow ⟨“ A B C ”⟩ \in (P^{(0 ..^3)}))$
85	82 83 84	mp2an	$⊢ (⟨“ A B C ”⟩ \in Word P \land \|⟨“ A B C ”⟩\| = 3) \leftrightarrow ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
86	80 81 85	sylanblc	$⊢ φ \to ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
87	8 9 10	s3cld	$⊢ φ \to ⟨“ D E F ”⟩ \in Word P$
88		s3len	$⊢ \|⟨“ D E F ”⟩\| = 3$
89		wrdmap	$⊢ (P \in V \land 3 \in ℕ_{0}) \to ((⟨“ D E F ”⟩ \in Word P \land \|⟨“ D E F ”⟩\| = 3) \leftrightarrow ⟨“ D E F ”⟩ \in (P^{(0 ..^3)}))$
90	82 83 89	mp2an	$⊢ (⟨“ D E F ”⟩ \in Word P \land \|⟨“ D E F ”⟩\| = 3) \leftrightarrow ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})$
91	87 88 90	sylanblc	$⊢ φ \to ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})$
92	86 91	jca	$⊢ φ \to (⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)}))$
93	92	biantrurd	$⊢ φ \to (\exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \leftrightarrow ((⟨“ A B C ”⟩ \in (P^{(0 ..^3)}) \land ⟨“ D E F ”⟩ \in (P^{(0 ..^3)})) \land \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)))$
94	46 79 93	3bitr4d	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$

Metamath Proof Explorer

Theorem iscgra

Proof