Metamath Proof Explorer


Theorem satffunlem2

Description: Lemma 2 for satffun : induction step. (Contributed by AV, 28-Oct-2023)

Ref Expression
Assertion satffunlem2 ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
2 simpr ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( 𝑀𝑉𝐸𝑊 ) )
3 peano2 ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
4 3 ancri ( 𝑁 ∈ ω → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) )
5 4 adantr ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) )
6 sssucid 𝑁 ⊆ suc 𝑁
7 6 a1i ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → 𝑁 ⊆ suc 𝑁 )
8 eqid ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
9 8 satfsschain ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) → ( 𝑁 ⊆ suc 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) )
10 9 imp ( ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) ∧ 𝑁 ⊆ suc 𝑁 ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
11 2 5 7 10 syl21anc ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) )
12 eqid ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) )
13 eqid { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) }
14 8 12 13 satffunlem2lem1 ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } )
15 14 expcom ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) )
16 11 15 syl ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) )
17 16 imp ( ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } )
18 8 12 13 satffunlem2lem2 ( ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) = ∅ )
19 funun ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) ∧ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) = ∅ ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) )
20 1 17 18 19 syl21anc ( ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) )
21 simpl ( ( 𝑀𝑉𝐸𝑊 ) → 𝑀𝑉 )
22 simpr ( ( 𝑀𝑉𝐸𝑊 ) → 𝐸𝑊 )
23 simpl ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → 𝑁 ∈ ω )
24 8 12 13 satfvsucsuc ( ( 𝑀𝑉𝐸𝑊𝑁 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) )
25 21 22 23 24 syl2an23an ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) )
26 25 funeqd ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ↔ Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) ) )
27 26 adantr ( ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ↔ Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀m ω ) ∣ ∀ 𝑗𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) } ) ) )
28 20 27 mpbird ( ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) )
29 28 ex ( ( 𝑁 ∈ ω ∧ ( 𝑀𝑉𝐸𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ) )