fmlasuc

Description: The valid Godel formulas of height ( N + 1 ) , expressed by the valid Godel formulas of height N . (Contributed by AV, 20-Sep-2023)

		Ref	Expression
	Assertion	fmlasuc	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		fmlasuc0	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) } ) )
2		eqid	⊢ ( ∅ Sat ∅ ) = ( ∅ Sat ∅ )
3	2	satf0op	⊢ ( 𝑁 ∈ ω → ( 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
4		fveq2	⊢ ( 𝑧 = 𝑤 → ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑤 ) )
5	4	oveq2d	⊢ ( 𝑧 = 𝑤 → ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) )
6	5	eqeq2d	⊢ ( 𝑧 = 𝑤 → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ↔ 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) )
7	6	cbvrexvw	⊢ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ↔ ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) )
8	7	orbi1i	⊢ ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) )
9		fmlafvel	⊢ ( 𝑁 ∈ ω → ( 𝑧 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
10	9	biimprd	⊢ ( 𝑁 ∈ ω → ( ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
11	10	adantld	⊢ ( 𝑁 ∈ ω → ( ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
12	11	imp	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) )
13		vex	⊢ 𝑧 ∈ V
14		0ex	⊢ ∅ ∈ V
15	13 14	op1std	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( 1^st ‘ 𝑦 ) = 𝑧 )
16	15	eleq1d	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( 1^st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
17	16	ad2antrl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( 1^st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) )
18	12 17	mpbird	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) )
19	18	3adant3	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) )
20		oveq1	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → ( 𝑢 ⊼_𝑔 𝑣 ) = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) )
21	20	eqeq2d	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → ( 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ↔ 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ) )
22	21	rexbidv	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ) )
23		eqidd	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → 𝑖 = 𝑖 )
24		id	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → 𝑢 = ( 1^st ‘ 𝑦 ) )
25	23 24	goaleq12d	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → ∀_𝑔 𝑖 𝑢 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) )
26	25	eqeq2d	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → ( 𝑥 = ∀_𝑔 𝑖 𝑢 ↔ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) )
27	26	rexbidv	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) )
28	22 27	orbi12d	⊢ ( 𝑢 = ( 1^st ‘ 𝑦 ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) )
29	28	adantl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) ∧ 𝑢 = ( 1^st ‘ 𝑦 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) )
30	2	satf0op	⊢ ( 𝑁 ∈ ω → ( 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) )
31		fmlafvel	⊢ ( 𝑁 ∈ ω → ( 𝑦 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
32	31	biimprd	⊢ ( 𝑁 ∈ ω → ( ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
33	32	adantld	⊢ ( 𝑁 ∈ ω → ( ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
34	33	imp	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) )
35		vex	⊢ 𝑦 ∈ V
36	35 14	op1std	⊢ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ → ( 1^st ‘ 𝑤 ) = 𝑦 )
37	36	eleq1d	⊢ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ → ( ( 1^st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
38	37	ad2antrl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( 1^st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) )
39	34 38	mpbird	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( 1^st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) )
40	39	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) → ( 1^st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) )
41		oveq2	⊢ ( 𝑣 = ( 1^st ‘ 𝑤 ) → ( 𝑧 ⊼_𝑔 𝑣 ) = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) )
42	41	eqeq2d	⊢ ( 𝑣 = ( 1^st ‘ 𝑤 ) → ( 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) )
43	42	adantl	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) ∧ 𝑣 = ( 1^st ‘ 𝑤 ) ) → ( 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) )
44		simpr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) → 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) )
45	40 43 44	rspcedvd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) )
46	45	exp31	⊢ ( 𝑁 ∈ ω → ( ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) ) )
47	46	exlimdv	⊢ ( 𝑁 ∈ ω → ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑦 , ∅ ⟩ ∧ ⟨ 𝑦 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) ) )
48	30 47	sylbid	⊢ ( 𝑁 ∈ ω → ( 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) ) )
49	48	rexlimdv	⊢ ( 𝑁 ∈ ω → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) )
50	49	adantr	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) )
51	15	oveq1d	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) )
52	51	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ↔ 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) )
53	52	rexbidv	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ↔ ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ) )
54	15	oveq1d	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) = ( 𝑧 ⊼_𝑔 𝑣 ) )
55	54	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) )
56	55	rexbidv	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) )
57	53 56	imbi12d	⊢ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) ) )
58	57	ad2antrl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼_𝑔 𝑣 ) ) ) )
59	50 58	mpbird	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ) )
60	59	orim1d	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) )
61	60	3impia	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) )
62	19 29 61	rspcedvd	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) )
63	62	3exp	⊢ ( 𝑁 ∈ ω → ( ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) ) )
64	63	exlimdv	⊢ ( 𝑁 ∈ ω → ( ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) ) )
65	8 64	syl7bi	⊢ ( 𝑁 ∈ ω → ( ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , ∅ ⟩ ∧ ⟨ 𝑧 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) ) )
66	3 65	sylbid	⊢ ( 𝑁 ∈ ω → ( 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) ) )
67	66	rexlimdv	⊢ ( 𝑁 ∈ ω → ( ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) )
68		fmlafvel	⊢ ( 𝑁 ∈ ω → ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑢 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
69	68	biimpa	⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ⟨ 𝑢 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
70	69	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) → ⟨ 𝑢 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
71		vex	⊢ 𝑢 ∈ V
72	71 14	op1std	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( 1^st ‘ 𝑦 ) = 𝑢 )
73	72	oveq1d	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) )
74	73	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ) )
75	74	rexbidv	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ) )
76		eqidd	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → 𝑖 = 𝑖 )
77	76 72	goaleq12d	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) = ∀_𝑔 𝑖 𝑢 )
78	77	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ↔ 𝑥 = ∀_𝑔 𝑖 𝑢 ) )
79	78	rexbidv	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) )
80	75 79	orbi12d	⊢ ( 𝑦 = ⟨ 𝑢 , ∅ ⟩ → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ↔ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) )
81	80	adantl	⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) ∧ 𝑦 = ⟨ 𝑢 , ∅ ⟩ ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ↔ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) )
82		fmlafvel	⊢ ( 𝑁 ∈ ω → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) ↔ ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
83	82	biimpd	⊢ ( 𝑁 ∈ ω → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
84	83	adantr	⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
85	84	imp	⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
86	85	adantr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ) → ⟨ 𝑣 , ∅ ⟩ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
87		vex	⊢ 𝑣 ∈ V
88	87 14	op1std	⊢ ( 𝑧 = ⟨ 𝑣 , ∅ ⟩ → ( 1^st ‘ 𝑧 ) = 𝑣 )
89	88	oveq2d	⊢ ( 𝑧 = ⟨ 𝑣 , ∅ ⟩ → ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) = ( 𝑢 ⊼_𝑔 𝑣 ) )
90	89	eqeq2d	⊢ ( 𝑧 = ⟨ 𝑣 , ∅ ⟩ → ( 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ) )
91	90	adantl	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ) ∧ 𝑧 = ⟨ 𝑣 , ∅ ⟩ ) → ( 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ) )
92		simpr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ) → 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) )
93	86 91 92	rspcedvd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ) → ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) )
94	93	rexlimdva2	⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) → ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ) )
95	94	orim1d	⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) )
96	95	imp	⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) )
97	70 81 96	rspcedvd	⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) → ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) )
98	97	rexlimdva2	⊢ ( 𝑁 ∈ ω → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) → ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ) )
99	67 98	impbid	⊢ ( 𝑁 ∈ ω → ( ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) ) )
100	99	abbidv	⊢ ( 𝑁 ∈ ω → { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) } )
101	100	uneq2d	⊢ ( 𝑁 ∈ ω → ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑦 ) ⊼_𝑔 ( 1^st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑦 ) ) } ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) } ) )
102	1 101	eqtrd	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼_𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑢 ) } ) )

Metamath Proof Explorer

Theorem fmlasuc

Proof