cgrabasimass

Description: The angle congruence relation is hereditary. (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	cgrabasimass	$⊢ φ \to \underset{˙}{\sim} [A] \subseteq 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		fveq1	$⊢ d = e \to d (0) = e (0)$
6		fveq1	$⊢ d = e \to d (1) = e (1)$
7	5 6	neeq12d	$⊢ d = e \to (d (0) \neq d (1) \leftrightarrow e (0) \neq e (1))$
8		fveq1	$⊢ d = e \to d (2) = e (2)$
9	6 8	neeq12d	$⊢ d = e \to (d (1) \neq d (2) \leftrightarrow e (1) \neq e (2))$
10	7 9	anbi12d	$⊢ d = e \to ((d (0) \neq d (1) \land d (1) \neq d (2)) \leftrightarrow (e (0) \neq e (1) \land e (1) \neq e (2)))$
11		imassrn	$⊢ \underset{˙}{\sim} [A] \subseteq ran \underset{˙}{\sim}$
12		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)))\})$
13		fvexd	$⊢ g = G \to {Base}_{g} \in V$
14		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
15	14 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
16		fvexd	$⊢ (g = G \land p = P) \to {hl}_{𝒢} (g) \in V$
17		fveq2	$⊢ g = G \to {hl}_{𝒢} (g) = {hl}_{𝒢} (G)$
18	17	adantr	$⊢ (g = G \land p = P) \to {hl}_{𝒢} (g) = {hl}_{𝒢} (G)$
19		oveq1	$⊢ p = P \to p^{(0 ..^3)} = P^{(0 ..^3)}$
20	19	ad2antlr	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to p^{(0 ..^3)} = P^{(0 ..^3)}$
21	20	eleq2d	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to (a \in (p^{(0 ..^3)}) \leftrightarrow a \in (P^{(0 ..^3)}))$
22	20	eleq2d	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to (b \in (p^{(0 ..^3)}) \leftrightarrow b \in (P^{(0 ..^3)}))$
23	21 22	anbi12d	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \leftrightarrow (a \in (P^{(0 ..^3)}) \land b \in (P^{(0 ..^3)})))$
24		simplr	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to p = P$
25		fveq2	$⊢ g = G \to \sim_{𝒢} (g) = \sim_{𝒢} (G)$
26	25	ad2antrr	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to \sim_{𝒢} (g) = \sim_{𝒢} (G)$
27	26	breqd	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \leftrightarrow a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩)$
28		fveq1	$⊢ k = {hl}_{𝒢} (G) \to k (b (1)) = {hl}_{𝒢} (G) (b (1))$
29	28	adantl	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to k (b (1)) = {hl}_{𝒢} (G) (b (1))$
30	29	breqd	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to (x k (b (1)) b (0) \leftrightarrow x {hl}_{𝒢} (G) (b (1)) b (0))$
31	29	breqd	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \to (y k (b (1)) b (2) \leftrightarrow y {hl}_{𝒢} (G) (b (1)) b (2))$
32	27 30 31	3anbi123d	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (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 {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2)))$
33	24 32	rexeqbidv	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (G)) \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 {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2)))$
34	24 33	rexeqbidv	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (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 {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2)))$
35	23 34	anbi12d	$⊢ ((g = G \land p = P) \land k = {hl}_{𝒢} (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 {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))$
36	16 18 35	sbcied2	$⊢ (g = G \land p = P) \to (\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 {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))$
37	13 15 36	sbcied2	$⊢ 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 {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))$
38		an21	$⊢ ((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 {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))) \leftrightarrow (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))$
39	37 38	bitrdi	$⊢ 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 (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2)))))$
40	39	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⟩ \| (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))\}$
41	4	elexd	$⊢ φ \to G \in V$
42		ovexd	$⊢ φ \to P^{(0 ..^3)} \in V$
43		simprrl	$⊢ (φ \land (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))) \to a \in (P^{(0 ..^3)})$
44		simprl	$⊢ (φ \land (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))) \to b \in (P^{(0 ..^3)})$
45	42 42 43 44	opabex2	$⊢ φ \to \{⟨a, b⟩ \| (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))\} \in V$
46	12 40 41 45	fvmptd3	$⊢ φ \to \sim_{𝒢}^{∠} (G) = \{⟨a, b⟩ \| (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))\}$
47	3 46	eqtrid	$⊢ φ \to \underset{˙}{\sim} = \{⟨a, b⟩ \| (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))\}$
48	47	rneqd	$⊢ φ \to ran \underset{˙}{\sim} = ran \{⟨a, b⟩ \| (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))\}$
49		rnopabss	$⊢ ran \{⟨a, b⟩ \| (b \in (P^{(0 ..^3)}) \land (a \in (P^{(0 ..^3)}) \land \exists x \in P \exists y \in P (a \sim_{𝒢} (G) ⟨“ x b (1) y ”⟩ \land x {hl}_{𝒢} (G) (b (1)) b (0) \land y {hl}_{𝒢} (G) (b (1)) b (2))))\} \subseteq P^{(0 ..^3)}$
50	48 49	eqsstrdi	$⊢ φ \to ran \underset{˙}{\sim} \subseteq P^{(0 ..^3)}$
51	11 50	sstrid	$⊢ φ \to \underset{˙}{\sim} [A] \subseteq P^{(0 ..^3)}$
52	51	sselda	$⊢ (φ \land e \in \underset{˙}{\sim} [A]) \to e \in (P^{(0 ..^3)})$
53	52	ad10antr	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e \in (P^{(0 ..^3)})$
54		eqid	$⊢ Itv (G) = Itv (G)$
55		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
56	4	ad7antr	$⊢ (((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \to G \in 𝒢_{Tarski}$
57	56	ad4antr	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to G \in 𝒢_{Tarski}$
58		simp-4r	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to u \in P$
59		simpllr	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to v \in P$
60		simplr	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to w \in P$
61		simp-8r	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to x \in P$
62		simp-7r	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to y \in P$
63		simp-6r	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to z \in P$
64	3	a1i	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
65		simp-9r	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to f \underset{˙}{\sim} e$
66	64 65	breqdi	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to f \sim_{𝒢}^{∠} (G) e$
67		simpr	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to f = ⟨“ u v w ”⟩$
68		simp-5r	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e = ⟨“ x y z ”⟩$
69	66 67 68	3brtr3d	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to ⟨“ u v w ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ x y z ”⟩$
70	1 54 55 57 58 59 60 61 62 63 69	cgrane3	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to y \neq x$
71	70	necomd	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to x \neq y$
72	68	fveq1d	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (0) = ⟨“ x y z ”⟩ (0)$
73		s3fv0	$⊢ x \in P \to ⟨“ x y z ”⟩ (0) = x$
74	61 73	syl	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to ⟨“ x y z ”⟩ (0) = x$
75	72 74	eqtrd	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (0) = x$
76	68	fveq1d	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (1) = ⟨“ x y z ”⟩ (1)$
77		s3fv1	$⊢ y \in P \to ⟨“ x y z ”⟩ (1) = y$
78	77	ad7antlr	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to ⟨“ x y z ”⟩ (1) = y$
79	76 78	eqtrd	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (1) = y$
80	71 75 79	3netr4d	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (0) \neq e (1)$
81	1 54 55 57 58 59 60 61 62 63 69	cgrane4	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to y \neq z$
82	68	fveq1d	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (2) = ⟨“ x y z ”⟩ (2)$
83		s3fv2	$⊢ z \in P \to ⟨“ x y z ”⟩ (2) = z$
84	63 83	syl	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to ⟨“ x y z ”⟩ (2) = z$
85	82 84	eqtrd	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (2) = z$
86	81 79 85	3netr4d	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e (1) \neq e (2)$
87	80 86	jca	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to (e (0) \neq e (1) \land e (1) \neq e (2))$
88	10 53 87	elrabd	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e \in \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
89	88 2	eleqtrrdi	$⊢ (((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land w \in P) \land f = ⟨“ u v w ”⟩) \to e \in A$
90	89	r19.29an	$⊢ ((((((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \land u \in P) \land v \in P) \land \exists w \in P f = ⟨“ u v w ”⟩) \to e \in A$
91	1	fvexi	$⊢ P \in V$
92		simp-6r	$⊢ (((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \to f \in A$
93	91 2 92	elcgrabasi	$⊢ (((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y 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))$
94		simpl	$⊢ (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w)) \to f = ⟨“ u v w ”⟩$
95	94	reximi	$⊢ \exists w \in P (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w)) \to \exists w \in P f = ⟨“ u v w ”⟩$
96	95	reximi	$⊢ \exists v \in P \exists w \in P (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w)) \to \exists v \in P \exists w \in P f = ⟨“ u v w ”⟩$
97	96	reximi	$⊢ \exists u \in P \exists v \in P \exists w \in P (f = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w)) \to \exists u \in P \exists v \in P \exists w \in P f = ⟨“ u v w ”⟩$
98	93 97	syl	$⊢ (((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \to \exists u \in P \exists v \in P \exists w \in P f = ⟨“ u v w ”⟩$
99	90 98	r19.29vva	$⊢ (((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land z \in P) \land e = ⟨“ x y z ”⟩) \to e \in A$
100	99	r19.29an	$⊢ ((((((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \land x \in P) \land y \in P) \land \exists z \in P e = ⟨“ x y z ”⟩) \to e \in A$
101	52	ad2antrr	$⊢ (((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \to e \in (P^{(0 ..^3)})$
102	91	s3rex	$⊢ e \in (P^{(0 ..^3)}) \leftrightarrow \exists x \in P \exists y \in P \exists z \in P e = ⟨“ x y z ”⟩$
103	101 102	sylib	$⊢ (((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \to \exists x \in P \exists y \in P \exists z \in P e = ⟨“ x y z ”⟩$
104	100 103	r19.29vva	$⊢ (((φ \land e \in \underset{˙}{\sim} [A]) \land f \in A) \land f \underset{˙}{\sim} e) \to e \in A$
105		vex	$⊢ e \in V$
106	105	elima	$⊢ e \in \underset{˙}{\sim} [A] \leftrightarrow \exists f \in A f \underset{˙}{\sim} e$
107	106	bilani	$⊢ (φ \land e \in \underset{˙}{\sim} [A]) \to \exists f \in A f \underset{˙}{\sim} e$
108	104 107	r19.29a	$⊢ (φ \land e \in \underset{˙}{\sim} [A]) \to e \in A$
109	108	ex	$⊢ φ \to (e \in \underset{˙}{\sim} [A] \to e \in A)$
110	109	ssrdv	$⊢ φ \to \underset{˙}{\sim} [A] \subseteq A$

Metamath Proof Explorer

Theorem cgrabasimass

Proof