Theorem goalrlem 35390

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

Assertion

Ref	Expression
goalrlem	⊢ (𝑁 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))))

Distinct variable groups:   𝑖,𝑁   𝑖,𝑎

Allowed substitution hint:   𝑁(𝑎)

Proof of Theorem goalrlem

Dummy variables 𝑗 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano2 7869	. . . . 5 ⊢ (𝑁 ∈ ω → suc 𝑁 ∈ ω)
2		df-goal 35336	. . . . . 6 ⊢ ∀𝑔𝑖𝑎 = ⟨2o, ⟨𝑖, 𝑎⟩⟩
3		opex 5427	. . . . . 6 ⊢ ⟨2o, ⟨𝑖, 𝑎⟩⟩ ∈ V
4	2, 3	eqeltri 2825	. . . . 5 ⊢ ∀𝑔𝑖𝑎 ∈ V
5		isfmlasuc 35382	. . . . 5 ⊢ ((suc 𝑁 ∈ ω ∧ ∀𝑔𝑖𝑎 ∈ V) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢))))
6	1, 4, 5	sylancl 586	. . . 4 ⊢ (𝑁 ∈ ω → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢))))
7	6	adantr 480	. . 3 ⊢ ((𝑁 ∈ ω ∧ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢))))
8		fmlasssuc 35383	. . . . . . . . . 10 ⊢ (suc 𝑁 ∈ ω → (Fmla‘suc 𝑁) ⊆ (Fmla‘suc suc 𝑁))
9	1, 8	syl 17	. . . . . . . . 9 ⊢ (𝑁 ∈ ω → (Fmla‘suc 𝑁) ⊆ (Fmla‘suc suc 𝑁))
10	9	sseld 3948	. . . . . . . 8 ⊢ (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
11	10	com12 32	. . . . . . 7 ⊢ (𝑎 ∈ (Fmla‘suc 𝑁) → (𝑁 ∈ ω → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
12	11	imim2i 16	. . . . . 6 ⊢ ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → (𝑁 ∈ ω → 𝑎 ∈ (Fmla‘suc suc 𝑁))))
13	12	com23 86	. . . . 5 ⊢ ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (𝑁 ∈ ω → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))))
14	13	impcom 407	. . . 4 ⊢ ((𝑁 ∈ ω ∧ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
15		gonanegoal 35346	. . . . . . . . . . 11 ⊢ (𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑖𝑎
16		eqneqall 2937	. . . . . . . . . . 11 ⊢ ((𝑢⊼𝑔𝑣) = ∀𝑔𝑖𝑎 → ((𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
17	15, 16	mpi 20	. . . . . . . . . 10 ⊢ ((𝑢⊼𝑔𝑣) = ∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc suc 𝑁))
18	17	eqcoms 2738	. . . . . . . . 9 ⊢ (∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc suc 𝑁))
19	18	a1i 11	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
20	19	rexlimdva 3135	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → (∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
21		df-goal 35336	. . . . . . . . . . . . 13 ⊢ ∀𝑔𝑗𝑢 = ⟨2o, ⟨𝑗, 𝑢⟩⟩
22	2, 21	eqeq12i 2748	. . . . . . . . . . . 12 ⊢ (∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 ↔ ⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨2o, ⟨𝑗, 𝑢⟩⟩)
23		2oex 8448	. . . . . . . . . . . . 13 ⊢ 2o ∈ V
24		opex 5427	. . . . . . . . . . . . 13 ⊢ ⟨𝑖, 𝑎⟩ ∈ V
25	23, 24	opth 5439	. . . . . . . . . . . 12 ⊢ (⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨2o, ⟨𝑗, 𝑢⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, 𝑎⟩ = ⟨𝑗, 𝑢⟩))
26	22, 25	bitri 275	. . . . . . . . . . 11 ⊢ (∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 ↔ (2o = 2o ∧ ⟨𝑖, 𝑎⟩ = ⟨𝑗, 𝑢⟩))
27		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑖 ∈ V
28		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
29	27, 28	opth 5439	. . . . . . . . . . . 12 ⊢ (⟨𝑖, 𝑎⟩ = ⟨𝑗, 𝑢⟩ ↔ (𝑖 = 𝑗 ∧ 𝑎 = 𝑢))
30		eleq1w 2812	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘suc 𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑁)))
31	30	eqcoms 2738	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘suc 𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑁)))
32	31, 11	biimtrdi 253	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘suc 𝑁) → (𝑁 ∈ ω → 𝑎 ∈ (Fmla‘suc suc 𝑁))))
33	32	impcomd 411	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑢 → ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
34	29, 33	simplbiim 504	. . . . . . . . . . 11 ⊢ (⟨𝑖, 𝑎⟩ = ⟨𝑗, 𝑢⟩ → ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
35	26, 34	simplbiim 504	. . . . . . . . . 10 ⊢ (∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
36	35	com12 32	. . . . . . . . 9 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
37	36	adantr 480	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑗 ∈ ω) → (∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
38	37	rexlimdva 3135	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → (∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
39	20, 38	jaod 859	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
40	39	rexlimdva 3135	. . . . 5 ⊢ (𝑁 ∈ ω → (∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
41	40	adantr 480	. . . 4 ⊢ ((𝑁 ∈ ω ∧ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) → (∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
42	14, 41	jaod 859	. . 3 ⊢ ((𝑁 ∈ ω ∧ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢)) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
43	7, 42	sylbid 240	. 2 ⊢ ((𝑁 ∈ ω ∧ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))
44	43	ex 412	1 ⊢ (𝑁 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∃wrex 3054  Vcvv 3450   ⊆ wss 3917  ⟨cop 4598  suc csuc 6337  ‘cfv 6514  (class class class)co 7390  ωcom 7845  2_oc2o 8431  ⊼_𝑔cgna 35328  ∀_𝑔cgol 35329  Fmlacfmla 35331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-map 8804  df-goel 35334  df-gona 35335  df-goal 35336  df-sat 35337  df-fmla 35339

This theorem is referenced by:  goalr  35391