Theorem satffunlem2lem2

Description: Lemma 2 for satffunlem2 . (Contributed by AV, 27-Oct-2023)

	Ref	Expression
Hypotheses	satffunlem2lem2.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
	satffunlem2lem2.a	⊢ 𝐴 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) )
	satffunlem2lem2.b	⊢ 𝐵 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) }
Assertion	satffunlem2lem2	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( dom ( 𝑆 ‘ suc 𝑁 ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		satffunlem2lem2.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
2		satffunlem2lem2.a	⊢ 𝐴 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) )
3		satffunlem2lem2.b	⊢ 𝐵 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) }
4	1	fveq1i	⊢ ( 𝑆 ‘ suc 𝑁 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 )
5	4	dmeqi	⊢ dom ( 𝑆 ‘ suc 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 )
6		simprl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝑀 ∈ 𝑉 )
7		simprr	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝐸 ∈ 𝑊 )
8		peano2	⊢ ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
9	8	adantr	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → suc 𝑁 ∈ ω )
10	6 7 9	3jca	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω ) )
11		satfdmfmla	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) = ( Fmla ‘ suc 𝑁 ) )
12	10 11	syl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) = ( Fmla ‘ suc 𝑁 ) )
13	12	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) = ( Fmla ‘ suc 𝑁 ) )
14	5 13	eqtrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → dom ( 𝑆 ‘ suc 𝑁 ) = ( Fmla ‘ suc 𝑁 ) )
15		ovex	⊢ ( 𝑀 ↑m ω ) ∈ V
16	15	difexi	⊢ ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ∈ V
17	2 16	eqeltri	⊢ 𝐴 ∈ V
18	17	a1i	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → 𝐴 ∈ V )
19	18	ralrimiva	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ∀ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝐴 ∈ V )
20	3 15	rabex2	⊢ 𝐵 ∈ V
21	20	a1i	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑖 ∈ ω ) → 𝐵 ∈ V )
22	21	ralrimiva	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ∀ 𝑖 ∈ ω 𝐵 ∈ V )
23	19 22	jca	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( ∀ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝐴 ∈ V ∧ ∀ 𝑖 ∈ ω 𝐵 ∈ V ) )
24	23	ralrimiva	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ∀ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∀ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝐴 ∈ V ∧ ∀ 𝑖 ∈ ω 𝐵 ∈ V ) )
25		simplr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) )
26	8	ancri	⊢ ( 𝑁 ∈ ω → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) )
27	26	ad2antrr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) )
28	25 27	jca	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) )
29		sssucid	⊢ 𝑁 ⊆ suc 𝑁
30	1	satfsschain	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) → ( 𝑁 ⊆ suc 𝑁 → ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) )
31	28 29 30	mpisyl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) )
32		dmopab3rexdif	⊢ ( ( ∀ 𝑢 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ∀ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝐴 ∈ V ∧ ∀ 𝑖 ∈ ω 𝐵 ∈ V ) ∧ ( 𝑆 ‘ 𝑁 ) ⊆ ( 𝑆 ‘ suc 𝑁 ) ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } = { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) } )
33	24 31 32	syl2anc	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } = { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) } )
34		simpr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
35		fveqeq2	⊢ ( 𝑤 = 𝑢 → ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑢 ) ↔ ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑢 ) ) )
36	35	adantl	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) ∧ 𝑤 = 𝑢 ) → ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑢 ) ↔ ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑢 ) ) )
37		eqidd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑢 ) )
38	34 36 37	rspcedvd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ∃ 𝑤 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑢 ) )
39	4	funeqi	⊢ ( Fun ( 𝑆 ‘ suc 𝑁 ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
40	39	biimpi	⊢ ( Fun ( 𝑆 ‘ suc 𝑁 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
41	40	adantl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
42	1	fveq1i	⊢ ( 𝑆 ‘ 𝑁 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 )
43	31 42 4	3sstr3g	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
44	41 43	jca	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) )
45	44	adantr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) )
46		funeldmdif	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( ( 1st ‘ 𝑢 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ↔ ∃ 𝑤 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑢 ) ) )
47	45 46	syl	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( ( 1st ‘ 𝑢 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ↔ ∃ 𝑤 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑢 ) ) )
48	38 47	mpbird	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑢 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
49	48	ex	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( 1st ‘ 𝑢 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
50	4 42	difeq12i	⊢ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
51	50	eleq2i	⊢ ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ↔ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
52	51	a1i	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ↔ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
53	13	eqcomd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ suc 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
54		simpl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝑁 ∈ ω )
55	6 7 54	3jca	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) )
56		satfdmfmla	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )
57	55 56	syl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )
58	57	eqcomd	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fmla ‘ 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
59	58	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
60	53 59	difeq12d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) = ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
61	60	eleq2d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 1st ‘ 𝑢 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ↔ ( 1st ‘ 𝑢 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
62	49 52 61	3imtr4d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( 1st ‘ 𝑢 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) )
63	62	imp	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑢 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
64	63	adantr	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) → ( 1st ‘ 𝑢 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
65		oveq1	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ( 𝑓 ⊼𝑔 𝑔 ) = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) )
66	65	eqeq2d	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ( 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ↔ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) )
67	66	rexbidv	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) )
68		eqidd	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → 𝑖 = 𝑖 )
69		id	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → 𝑓 = ( 1st ‘ 𝑢 ) )
70	68 69	goaleq12d	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ∀𝑔 𝑖 𝑓 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) )
71	70	eqeq2d	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ( 𝑥 = ∀𝑔 𝑖 𝑓 ↔ 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
72	71	rexbidv	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
73	67 72	orbi12d	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
74	73	adantl	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ∧ 𝑓 = ( 1st ‘ 𝑢 ) ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
75	6	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → 𝑀 ∈ 𝑉 )
76	7	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → 𝐸 ∈ 𝑊 )
77	8	ad2antrr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → suc 𝑁 ∈ ω )
78	75 76 77	3jca	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω ) )
79		satfrel	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
80	78 79	syl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
81	4	releqi	⊢ ( Rel ( 𝑆 ‘ suc 𝑁 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
82	80 81	sylibr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → Rel ( 𝑆 ‘ suc 𝑁 ) )
83		1stdm	⊢ ( ( Rel ( 𝑆 ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 1st ‘ 𝑣 ) ∈ dom ( 𝑆 ‘ suc 𝑁 ) )
84	82 83	sylan	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 1st ‘ 𝑣 ) ∈ dom ( 𝑆 ‘ suc 𝑁 ) )
85	14	eqcomd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ suc 𝑁 ) = dom ( 𝑆 ‘ suc 𝑁 ) )
86	85	adantr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ suc 𝑁 ) = dom ( 𝑆 ‘ suc 𝑁 ) )
87	84 86	eleqtrrd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) → ( 1st ‘ 𝑣 ) ∈ ( Fmla ‘ suc 𝑁 ) )
88	87	ad4ant13	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ( 1st ‘ 𝑣 ) ∈ ( Fmla ‘ suc 𝑁 ) )
89		oveq2	⊢ ( 𝑔 = ( 1st ‘ 𝑣 ) → ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) )
90	89	eqeq2d	⊢ ( 𝑔 = ( 1st ‘ 𝑣 ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
91	90	adantl	⊢ ( ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ∧ 𝑔 = ( 1st ‘ 𝑣 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
92		simpr	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) )
93	88 91 92	rspcedvd	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) )
94	93	rexlimdva2	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) → ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) )
95	94	orim1d	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) → ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
96	95	imp	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) → ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
97	64 74 96	rspcedvd	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) → ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) )
98	97	rexlimdva2	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) → ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) )
99	55	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) )
100		satfrel	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
101	99 100	syl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
102	42	releqi	⊢ ( Rel ( 𝑆 ‘ 𝑁 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
103	101 102	sylibr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → Rel ( 𝑆 ‘ 𝑁 ) )
104		1stdm	⊢ ( ( Rel ( 𝑆 ‘ 𝑁 ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) → ( 1st ‘ 𝑢 ) ∈ dom ( 𝑆 ‘ 𝑁 ) )
105	103 104	sylan	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) → ( 1st ‘ 𝑢 ) ∈ dom ( 𝑆 ‘ 𝑁 ) )
106	42	dmeqi	⊢ dom ( 𝑆 ‘ 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 )
107	99 56	syl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )
108	106 107	eqtrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → dom ( 𝑆 ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )
109	108	eqcomd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ 𝑁 ) = dom ( 𝑆 ‘ 𝑁 ) )
110	109	adantr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) → ( Fmla ‘ 𝑁 ) = dom ( 𝑆 ‘ 𝑁 ) )
111	105 110	eleqtrrd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) → ( 1st ‘ 𝑢 ) ∈ ( Fmla ‘ 𝑁 ) )
112	111	adantr	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ( 1st ‘ 𝑢 ) ∈ ( Fmla ‘ 𝑁 ) )
113	66	rexbidv	⊢ ( 𝑓 = ( 1st ‘ 𝑢 ) → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) )
114	113	adantl	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ∧ 𝑓 = ( 1st ‘ 𝑢 ) ) → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) )
115		simpr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
116		fveqeq2	⊢ ( 𝑡 = 𝑣 → ( ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑣 ) ↔ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑣 ) ) )
117	116	adantl	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) ∧ 𝑡 = 𝑣 ) → ( ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑣 ) ↔ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑣 ) ) )
118		eqidd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑣 ) )
119	115 117 118	rspcedvd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ∃ 𝑡 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑣 ) )
120	44	adantr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) )
121		funeldmdif	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( ( 1st ‘ 𝑣 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ↔ ∃ 𝑡 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑣 ) ) )
122	120 121	syl	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( ( 1st ‘ 𝑣 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ↔ ∃ 𝑡 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑣 ) ) )
123	119 122	mpbird	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑣 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
124	123	ex	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( 1st ‘ 𝑣 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
125	50	eleq2i	⊢ ( 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ↔ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
126	125	a1i	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ↔ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
127	12	eqcomd	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fmla ‘ suc 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
128	127 58	difeq12d	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) = ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
129	128	eleq2d	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 1st ‘ 𝑣 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ↔ ( 1st ‘ 𝑣 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
130	129	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 1st ‘ 𝑣 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ↔ ( 1st ‘ 𝑣 ) ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
131	124 126 130	3imtr4d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( 1st ‘ 𝑣 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) )
132	131	adantr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) → ( 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) → ( 1st ‘ 𝑣 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ) )
133	132	imp	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑣 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
134	133	adantr	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ( 1st ‘ 𝑣 ) ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) )
135	90	adantl	⊢ ( ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ∧ 𝑔 = ( 1st ‘ 𝑣 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
136		simpr	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) )
137	134 135 136	rspcedvd	⊢ ( ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) )
138	137	r19.29an	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) )
139	112 114 138	rspcedvd	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) ∧ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) )
140	139	rexlimdva2	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) → ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) )
141	98 140	orim12d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) → ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) ) )
142	10	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω ) )
143	11	eqcomd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω ) → ( Fmla ‘ suc 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
144	142 143	syl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ suc 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
145	107	eqcomd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
146	144 145	difeq12d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) = ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
147	146	eleq2d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ↔ 𝑓 ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
148		eqid	⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
149	148	satfsschain	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) → ( 𝑁 ⊆ suc 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) )
150	28 29 149	mpisyl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
151		releldmdifi	⊢ ( ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 ) )
152	80 150 151	syl2anc	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 ) )
153	147 152	sylbid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 ) )
154	50	eqcomi	⊢ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) = ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) )
155	154	rexeqi	⊢ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 ↔ ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 )
156		r19.41v	⊢ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) ↔ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) )
157		oveq1	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) = ( 𝑓 ⊼𝑔 𝑔 ) )
158	157	eqeq2d	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) )
159	158	rexbidv	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) )
160		eqidd	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → 𝑖 = 𝑖 )
161		id	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( 1st ‘ 𝑢 ) = 𝑓 )
162	160 161	goaleq12d	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) = ∀𝑔 𝑖 𝑓 )
163	162	eqeq2d	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ↔ 𝑥 = ∀𝑔 𝑖 𝑓 ) )
164	163	rexbidv	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) )
165	159 164	orbi12d	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) )
166	165	adantl	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( 1st ‘ 𝑢 ) = 𝑓 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) )
167	142 11	syl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) = ( Fmla ‘ suc 𝑁 ) )
168	167	eqcomd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( Fmla ‘ suc 𝑁 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
169	168	eleq2d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝑔 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) )
170		releldm2	⊢ ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → ( 𝑔 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 1st ‘ 𝑣 ) = 𝑔 ) )
171	80 170	syl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 1st ‘ 𝑣 ) = 𝑔 ) )
172	169 171	bitrd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 1st ‘ 𝑣 ) = 𝑔 ) )
173		r19.41v	⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) ↔ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) )
174	1	eqcomi	⊢ ( 𝑀 Sat 𝐸 ) = 𝑆
175	174	fveq1i	⊢ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) = ( 𝑆 ‘ suc 𝑁 )
176	175	rexeqi	⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) ↔ ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) )
177	89	eqcoms	⊢ ( ( 1st ‘ 𝑣 ) = 𝑔 → ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) )
178	177	eqeq2d	⊢ ( ( 1st ‘ 𝑣 ) = 𝑔 → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
179	178	biimpa	⊢ ( ( ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) → 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) )
180	179	a1i	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) → 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
181	180	reximdv	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
182	176 181	biimtrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
183	173 182	biimtrrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 1st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
184	183	expd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 1st ‘ 𝑣 ) = 𝑔 → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
185	172 184	sylbid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
186	185	rexlimdv	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
187	186	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( 1st ‘ 𝑢 ) = 𝑓 ) → ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
188	187	orim1d	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( 1st ‘ 𝑢 ) = 𝑓 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
189	166 188	sylbird	⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) ∧ ( 1st ‘ 𝑢 ) = 𝑓 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
190	189	expimpd	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ) → ( ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
191	190	reximdva	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) → ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
192	156 191	biimtrrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ) → ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
193	192	expd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) → ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ) )
194	155 193	biimtrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑢 ) = 𝑓 → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) → ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ) )
195	153 194	syld	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) → ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) ) )
196	195	rexlimdv	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) → ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
197	145	eleq2d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑓 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
198	55 100	syl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
199	198	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
200		releldm2	⊢ ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( 𝑓 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 1st ‘ 𝑢 ) = 𝑓 ) )
201	199 200	syl	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 1st ‘ 𝑢 ) = 𝑓 ) )
202	197 201	bitrd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 1st ‘ 𝑢 ) = 𝑓 ) )
203		r19.41v	⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) ↔ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) )
204	42	eqcomi	⊢ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( 𝑆 ‘ 𝑁 )
205	204	rexeqi	⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) )
206	158	rexbidv	⊢ ( ( 1st ‘ 𝑢 ) = 𝑓 → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) )
207	206	adantl	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 1st ‘ 𝑢 ) = 𝑓 ) → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) )
208	146	eleq2d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ↔ 𝑔 ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
209		releldmdifi	⊢ ( ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 ) )
210	80 150 209	syl2anc	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 ) )
211	208 210	sylbid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 ) )
212	154	rexeqi	⊢ ( ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 ↔ ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 )
213	178	biimpcd	⊢ ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ( ( 1st ‘ 𝑣 ) = 𝑔 → 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
214	213	adantl	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) → ( ( 1st ‘ 𝑣 ) = 𝑔 → 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
215	214	reximdv	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
216	215	ex	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
217	216	com23	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
218	212 217	biimtrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 1st ‘ 𝑣 ) = 𝑔 → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
219	211 218	syld	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
220	219	rexlimdv	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
221	220	adantr	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 1st ‘ 𝑢 ) = 𝑓 ) → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
222	207 221	sylbird	⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) ∧ ( 1st ‘ 𝑢 ) = 𝑓 ) → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
223	222	expimpd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) → ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
224	223	reximdv	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
225	205 224	biimtrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
226	203 225	biimtrrid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 1st ‘ 𝑢 ) = 𝑓 ∧ ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) → ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
227	226	expd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 1st ‘ 𝑢 ) = 𝑓 → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) → ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
228	202 227	sylbid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( 𝑓 ∈ ( Fmla ‘ 𝑁 ) → ( ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) → ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
229	228	rexlimdv	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) → ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) )
230	196 229	orim12d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ) )
231	141 230	impbid	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) ↔ ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) ) )
232	231	abbidv	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → { 𝑥 ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) } = { 𝑥 ∣ ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) } )
233	33 232	eqtrd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } = { 𝑥 ∣ ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) } )
234	14 233	ineq12d	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( dom ( 𝑆 ‘ suc 𝑁 ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) = ( ( Fmla ‘ suc 𝑁 ) ∩ { 𝑥 ∣ ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) } ) )
235		fmlasucdisj	⊢ ( 𝑁 ∈ ω → ( ( Fmla ‘ suc 𝑁 ) ∩ { 𝑥 ∣ ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) } ) = ∅ )
236	235	ad2antrr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( ( Fmla ‘ suc 𝑁 ) ∩ { 𝑥 ∣ ( ∃ 𝑓 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) ( ∃ 𝑔 ∈ ( Fmla ‘ suc 𝑁 ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑓 ) ∨ ∃ 𝑓 ∈ ( Fmla ‘ 𝑁 ) ∃ 𝑔 ∈ ( ( Fmla ‘ suc 𝑁 ) ∖ ( Fmla ‘ 𝑁 ) ) 𝑥 = ( 𝑓 ⊼𝑔 𝑔 ) ) } ) = ∅ )
237	234 236	eqtrd	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( 𝑆 ‘ suc 𝑁 ) ) → ( dom ( 𝑆 ‘ suc 𝑁 ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = 𝐵 ) ) ∨ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( 𝑆 ‘ suc 𝑁 ) ∖ ( 𝑆 ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) = ∅ )