gonarlem

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

		Ref	Expression
	Assertion	gonarlem	$⊢ N \in ω \to ((a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N))) \to (a ⊼_{𝑔} b \in Fmla (suc suc N) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$

Proof

Step	Hyp	Ref	Expression
1		peano2	$⊢ N \in ω \to suc N \in ω$
2		ovexd	$⊢ N \in ω \to a ⊼_{𝑔} b \in V$
3		isfmlasuc	$⊢ (suc N \in ω \land a ⊼_{𝑔} b \in V) \to (a ⊼_{𝑔} b \in Fmla (suc suc N) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u])))$
4	1 2 3	syl2anc	$⊢ N \in ω \to (a ⊼_{𝑔} b \in Fmla (suc suc N) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u])))$
5	4	adantr	$⊢ (N \in ω \land (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N)))) \to (a ⊼_{𝑔} b \in Fmla (suc suc N) \leftrightarrow (a ⊼_{𝑔} b \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u])))$
6		fmlasssuc	$⊢ suc N \in ω \to Fmla (suc N) \subseteq Fmla (suc suc N)$
7	1 6	syl	$⊢ N \in ω \to Fmla (suc N) \subseteq Fmla (suc suc N)$
8	7	sseld	$⊢ N \in ω \to (a \in Fmla (suc N) \to a \in Fmla (suc suc N))$
9	7	sseld	$⊢ N \in ω \to (b \in Fmla (suc N) \to b \in Fmla (suc suc N))$
10	8 9	anim12d	$⊢ N \in ω \to ((a \in Fmla (suc N) \land b \in Fmla (suc N)) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
11	10	com12	$⊢ (a \in Fmla (suc N) \land b \in Fmla (suc N)) \to (N \in ω \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
12	11	imim2i	$⊢ (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N))) \to (a ⊼_{𝑔} b \in Fmla (suc N) \to (N \in ω \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$
13	12	com23	$⊢ (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N))) \to (N \in ω \to (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$
14	13	impcom	$⊢ (N \in ω \land (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N)))) \to (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
15		gonafv	$⊢ (a \in V \land b \in V) \to a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
16	15	el2v	$⊢ a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
17	16	a1i	$⊢ (u \in Fmla (suc N) \land v \in Fmla (suc N)) \to a ⊼_{𝑔} b = ⟨1_{𝑜}, ⟨a, b⟩⟩$
18		gonafv	$⊢ (u \in Fmla (suc N) \land v \in Fmla (suc N)) \to u ⊼_{𝑔} v = ⟨1_{𝑜}, ⟨u, v⟩⟩$
19	17 18	eqeq12d	$⊢ (u \in Fmla (suc N) \land v \in Fmla (suc N)) \to (a ⊼_{𝑔} b = u ⊼_{𝑔} v \leftrightarrow ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩)$
20		1oex	$⊢ 1_{𝑜} \in V$
21		opex	$⊢ ⟨a, b⟩ \in V$
22	20 21	opth	$⊢ ⟨1_{𝑜}, ⟨a, b⟩⟩ = ⟨1_{𝑜}, ⟨u, v⟩⟩ \leftrightarrow (1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩)$
23	19 22	bitrdi	$⊢ (u \in Fmla (suc N) \land v \in Fmla (suc N)) \to (a ⊼_{𝑔} b = u ⊼_{𝑔} v \leftrightarrow (1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩))$
24	23	adantll	$⊢ ((N \in ω \land u \in Fmla (suc N)) \land v \in Fmla (suc N)) \to (a ⊼_{𝑔} b = u ⊼_{𝑔} v \leftrightarrow (1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩))$
25		vex	$⊢ a \in V$
26		vex	$⊢ b \in V$
27	25 26	opth	$⊢ ⟨a, b⟩ = ⟨u, v⟩ \leftrightarrow (a = u \land b = v)$
28		eleq1w	$⊢ u = a \to (u \in Fmla (suc N) \leftrightarrow a \in Fmla (suc N))$
29	28	equcoms	$⊢ a = u \to (u \in Fmla (suc N) \leftrightarrow a \in Fmla (suc N))$
30		eleq1w	$⊢ v = b \to (v \in Fmla (suc N) \leftrightarrow b \in Fmla (suc N))$
31	30	equcoms	$⊢ b = v \to (v \in Fmla (suc N) \leftrightarrow b \in Fmla (suc N))$
32	29 31	bi2anan9	$⊢ (a = u \land b = v) \to ((u \in Fmla (suc N) \land v \in Fmla (suc N)) \leftrightarrow (a \in Fmla (suc N) \land b \in Fmla (suc N)))$
33	32 11	syl6bi	$⊢ (a = u \land b = v) \to ((u \in Fmla (suc N) \land v \in Fmla (suc N)) \to (N \in ω \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$
34	27 33	sylbi	$⊢ ⟨a, b⟩ = ⟨u, v⟩ \to ((u \in Fmla (suc N) \land v \in Fmla (suc N)) \to (N \in ω \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$
35	34	adantl	$⊢ (1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩) \to ((u \in Fmla (suc N) \land v \in Fmla (suc N)) \to (N \in ω \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$
36	35	com13	$⊢ N \in ω \to ((u \in Fmla (suc N) \land v \in Fmla (suc N)) \to ((1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$
37	36	impl	$⊢ ((N \in ω \land u \in Fmla (suc N)) \land v \in Fmla (suc N)) \to ((1_{𝑜} = 1_{𝑜} \land ⟨a, b⟩ = ⟨u, v⟩) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
38	24 37	sylbid	$⊢ ((N \in ω \land u \in Fmla (suc N)) \land v \in Fmla (suc N)) \to (a ⊼_{𝑔} b = u ⊼_{𝑔} v \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
39	38	rexlimdva	$⊢ (N \in ω \land u \in Fmla (suc N)) \to (\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
40		gonanegoal	$⊢ a ⊼_{𝑔} b \neq [\forall_{𝑔} i u]$
41		eqneqall	$⊢ a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a ⊼_{𝑔} b \neq [\forall_{𝑔} i u] \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
42	40 41	mpi	$⊢ a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))$
43	42	a1i	$⊢ ((N \in ω \land u \in Fmla (suc N)) \land i \in ω) \to (a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
44	43	rexlimdva	$⊢ (N \in ω \land u \in Fmla (suc N)) \to (\exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u] \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
45	39 44	jaod	$⊢ (N \in ω \land u \in Fmla (suc N)) \to ((\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u]) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
46	45	rexlimdva	$⊢ N \in ω \to (\exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u]) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
47	46	adantr	$⊢ (N \in ω \land (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N)))) \to (\exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u]) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
48	14 47	jaod	$⊢ (N \in ω \land (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N)))) \to ((a ⊼_{𝑔} b \in Fmla (suc N) \lor \exists u \in Fmla (suc N) (\exists v \in Fmla (suc N) a ⊼_{𝑔} b = u ⊼_{𝑔} v \lor \exists i \in ω a ⊼_{𝑔} b = [\forall_{𝑔} i u])) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
49	5 48	sylbid	$⊢ (N \in ω \land (a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N)))) \to (a ⊼_{𝑔} b \in Fmla (suc suc N) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N)))$
50	49	ex	$⊢ N \in ω \to ((a ⊼_{𝑔} b \in Fmla (suc N) \to (a \in Fmla (suc N) \land b \in Fmla (suc N))) \to (a ⊼_{𝑔} b \in Fmla (suc suc N) \to (a \in Fmla (suc suc N) \land b \in Fmla (suc suc N))))$

Metamath Proof Explorer

Theorem gonarlem

Proof