goalrlem

Description: Lemma for goalr (induction step). (Contributed by AV, 22-Oct-2023)

		Ref	Expression
	Assertion	goalrlem	$⊢ N \in ω \to (([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N)) \to ([\forall_{𝑔} i a] \in Fmla (suc suc N) \to a \in Fmla (suc suc N)))$

Proof

Step	Hyp	Ref	Expression
1		peano2	$⊢ N \in ω \to suc N \in ω$
2		df-goal	$⊢ [\forall_{𝑔} i a] = ⟨2_{𝑜}, ⟨i, a⟩⟩$
3		opex	$⊢ ⟨2_{𝑜}, ⟨i, a⟩⟩ \in V$
4	2 3	eqeltri	$⊢ [\forall_{𝑔} i a] \in V$
5		isfmlasuc	$⊢ (suc N \in ω \land [\forall_{𝑔} i a] \in V) \to ([\forall_{𝑔} i a] \in Fmla (suc suc N) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u])))$
6	1 4 5	sylancl	$⊢ N \in ω \to ([\forall_{𝑔} i a] \in Fmla (suc suc N) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u])))$
7	6	adantr	$⊢ (N \in ω \land ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N))) \to ([\forall_{𝑔} i a] \in Fmla (suc suc N) \leftrightarrow ([\forall_{𝑔} i a] \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u])))$
8		fmlasssuc	$⊢ suc N \in ω \to Fmla (suc N) \subseteq Fmla (suc suc N)$
9	1 8	syl	$⊢ N \in ω \to Fmla (suc N) \subseteq Fmla (suc suc N)$
10	9	sseld	$⊢ N \in ω \to (a \in Fmla (suc N) \to a \in Fmla (suc suc N))$
11	10	com12	$⊢ a \in Fmla (suc N) \to (N \in ω \to a \in Fmla (suc suc N))$
12	11	imim2i	$⊢ ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N)) \to ([\forall_{𝑔} i a] \in Fmla (suc N) \to (N \in ω \to a \in Fmla (suc suc N)))$
13	12	com23	$⊢ ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N)) \to (N \in ω \to ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc suc N)))$
14	13	impcom	$⊢ (N \in ω \land ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N))) \to ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc suc N))$
15		gonanegoal	$⊢ u ⊼_{𝑔} v \neq [\forall_{𝑔} i a]$
16		eqneqall	$⊢ u ⊼_{𝑔} v = [\forall_{𝑔} i a] \to (u ⊼_{𝑔} v \neq [\forall_{𝑔} i a] \to a \in Fmla (suc suc N))$
17	15 16	mpi	$⊢ u ⊼_{𝑔} v = [\forall_{𝑔} i a] \to a \in Fmla (suc suc N)$
18	17	eqcoms	$⊢ [\forall_{𝑔} i a] = u ⊼_{𝑔} v \to a \in Fmla (suc suc N)$
19	18	a1i	$⊢ ((N \in ω \land u \in Fmla (suc N)) \land v \in Fmla (suc N)) \to ([\forall_{𝑔} i a] = u ⊼_{𝑔} v \to a \in Fmla (suc suc N))$
20	19	rexlimdva	$⊢ (N \in ω \land u \in Fmla (suc N)) \to (\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \to a \in Fmla (suc suc N))$
21		df-goal	$⊢ [\forall_{𝑔} j u] = ⟨2_{𝑜}, ⟨j, u⟩⟩$
22	2 21	eqeq12i	$⊢ [\forall_{𝑔} i a] = [\forall_{𝑔} j u] \leftrightarrow ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨2_{𝑜}, ⟨j, u⟩⟩$
23		2oex	$⊢ 2_{𝑜} \in V$
24		opex	$⊢ ⟨i, a⟩ \in V$
25	23 24	opth	$⊢ ⟨2_{𝑜}, ⟨i, a⟩⟩ = ⟨2_{𝑜}, ⟨j, u⟩⟩ \leftrightarrow (2_{𝑜} = 2_{𝑜} \land ⟨i, a⟩ = ⟨j, u⟩)$
26	22 25	bitri	$⊢ [\forall_{𝑔} i a] = [\forall_{𝑔} j u] \leftrightarrow (2_{𝑜} = 2_{𝑜} \land ⟨i, a⟩ = ⟨j, u⟩)$
27		vex	$⊢ i \in V$
28		vex	$⊢ a \in V$
29	27 28	opth	$⊢ ⟨i, a⟩ = ⟨j, u⟩ \leftrightarrow (i = j \land a = u)$
30		eleq1w	$⊢ u = a \to (u \in Fmla (suc N) \leftrightarrow a \in Fmla (suc N))$
31	30	eqcoms	$⊢ a = u \to (u \in Fmla (suc N) \leftrightarrow a \in Fmla (suc N))$
32	31 11	syl6bi	$⊢ a = u \to (u \in Fmla (suc N) \to (N \in ω \to a \in Fmla (suc suc N)))$
33	32	impcomd	$⊢ a = u \to ((N \in ω \land u \in Fmla (suc N)) \to a \in Fmla (suc suc N))$
34	29 33	simplbiim	$⊢ ⟨i, a⟩ = ⟨j, u⟩ \to ((N \in ω \land u \in Fmla (suc N)) \to a \in Fmla (suc suc N))$
35	26 34	simplbiim	$⊢ [\forall_{𝑔} i a] = [\forall_{𝑔} j u] \to ((N \in ω \land u \in Fmla (suc N)) \to a \in Fmla (suc suc N))$
36	35	com12	$⊢ (N \in ω \land u \in Fmla (suc N)) \to ([\forall_{𝑔} i a] = [\forall_{𝑔} j u] \to a \in Fmla (suc suc N))$
37	36	adantr	$⊢ ((N \in ω \land u \in Fmla (suc N)) \land j \in ω) \to ([\forall_{𝑔} i a] = [\forall_{𝑔} j u] \to a \in Fmla (suc suc N))$
38	37	rexlimdva	$⊢ (N \in ω \land u \in Fmla (suc N)) \to (\exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u] \to a \in Fmla (suc suc N))$
39	20 38	jaod	$⊢ (N \in ω \land u \in Fmla (suc N)) \to ((\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u]) \to a \in Fmla (suc suc N))$
40	39	rexlimdva	$⊢ N \in ω \to (\exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u]) \to a \in Fmla (suc suc N))$
41	40	adantr	$⊢ (N \in ω \land ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N))) \to (\exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u]) \to a \in Fmla (suc suc N))$
42	14 41	jaod	$⊢ (N \in ω \land ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N))) \to (([\forall_{𝑔} i a] \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) [\forall_{𝑔} i a] = u ⊼_{𝑔} v \lor \exists j \in ω [\forall_{𝑔} i a] = [\forall_{𝑔} j u])) \to a \in Fmla (suc suc N))$
43	7 42	sylbid	$⊢ (N \in ω \land ([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N))) \to ([\forall_{𝑔} i a] \in Fmla (suc suc N) \to a \in Fmla (suc suc N))$
44	43	ex	$⊢ N \in ω \to (([\forall_{𝑔} i a] \in Fmla (suc N) \to a \in Fmla (suc N)) \to ([\forall_{𝑔} i a] \in Fmla (suc suc N) \to a \in Fmla (suc suc N)))$

Metamath Proof Explorer

Theorem goalrlem

Proof