inagcgratrgw

Description: inagcgratrgmain with the existential introduced at its own witness Q . Split out so that the substitution instance is built once, at the top level, rather than under the existential eliminations that produce S , T and Q . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagcgratrgmain.p	$⊢ P = {Base}_{G}$
	inagcgratrgmain.i	$⊢ I = Itv (G)$
	inagcgratrgmain.k	$⊢ K = {hl}_{𝒢} (G)$
	inagcgratrgmain.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagcgratrgmain.d	$⊢ φ \to D \in P$
	inagcgratrgmain.e	$⊢ φ \to E \in P$
	inagcgratrgmain.w	$⊢ φ \to W \in P$
	inagcgratrgmain.x	$⊢ φ \to X \in P$
	inagcgratrgmain.y	$⊢ φ \to Y \in P$
	inagcgratrgmain.z	$⊢ φ \to Z \in P$
	inagcgratrgmain.j	$⊢ φ \to J \in P$
	inagcgratrgmain.s	$⊢ φ \to S \in P$
	inagcgratrgmain.t	$⊢ φ \to T \in P$
	inagcgratrgmain.q	$⊢ φ \to Q \in P$
	inagcgratrgmain.de	$⊢ φ \to D \neq E$
	inagcgratrgmain.jw	$⊢ φ \to J K (E) W$
	inagcgratrgmain.sx	$⊢ φ \to S K (Y) X$
	inagcgratrgmain.tz	$⊢ φ \to T K (Y) Z$
	inagcgratrgmain.q1	$⊢ φ \to Q \in (S I T)$
	inagcgratrgmain.sub	$⊢ φ \to ⟨“ D E J ”⟩ \sim_{𝒢} (G) ⟨“ S Y Q ”⟩$
Assertion	inagcgratrgw	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		inagcgratrgmain.p	$⊢ P = {Base}_{G}$
2		inagcgratrgmain.i	$⊢ I = Itv (G)$
3		inagcgratrgmain.k	$⊢ K = {hl}_{𝒢} (G)$
4		inagcgratrgmain.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		inagcgratrgmain.d	$⊢ φ \to D \in P$
6		inagcgratrgmain.e	$⊢ φ \to E \in P$
7		inagcgratrgmain.w	$⊢ φ \to W \in P$
8		inagcgratrgmain.x	$⊢ φ \to X \in P$
9		inagcgratrgmain.y	$⊢ φ \to Y \in P$
10		inagcgratrgmain.z	$⊢ φ \to Z \in P$
11		inagcgratrgmain.j	$⊢ φ \to J \in P$
12		inagcgratrgmain.s	$⊢ φ \to S \in P$
13		inagcgratrgmain.t	$⊢ φ \to T \in P$
14		inagcgratrgmain.q	$⊢ φ \to Q \in P$
15		inagcgratrgmain.de	$⊢ φ \to D \neq E$
16		inagcgratrgmain.jw	$⊢ φ \to J K (E) W$
17		inagcgratrgmain.sx	$⊢ φ \to S K (Y) X$
18		inagcgratrgmain.tz	$⊢ φ \to T K (Y) Z$
19		inagcgratrgmain.q1	$⊢ φ \to Q \in (S I T)$
20		inagcgratrgmain.sub	$⊢ φ \to ⟨“ D E J ”⟩ \sim_{𝒢} (G) ⟨“ S Y Q ”⟩$
21		simpr	$⊢ (φ \land v = Q) \to v = Q$
22	21	breq1d	$⊢ (φ \land v = Q) \to (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \leftrightarrow Q \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩)$
23		eqidd	$⊢ (φ \land v = Q) \to X = X$
24		eqidd	$⊢ (φ \land v = Q) \to Y = Y$
25	23 24 21	s3eqd	$⊢ (φ \land v = Q) \to ⟨“ X Y v ”⟩ = ⟨“ X Y Q ”⟩$
26	25	breq2d	$⊢ (φ \land v = Q) \to (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \leftrightarrow ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Q ”⟩)$
27	22 26	anbi12d	$⊢ (φ \land v = Q) \to ((v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩) \leftrightarrow (Q \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Q ”⟩))$
28		eqid	$⊢ dist (G) = dist (G)$
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 28	inagcgratrgmain	$⊢ φ \to (Q \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Q ”⟩)$
30	14 27 29	rspcedvd	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Metamath Proof Explorer

Theorem inagcgratrgw

Proof