This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑣 ) ) ∧ 𝑦 = 𝐴 ) ) } ) = ∅ )