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 ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
13		eqid	⊢ { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) }
14	8 12 13	satffunlem2lem1	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } )
15	14	expcom	⊢ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) )
16	11 15	syl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) )
17	16	imp	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } )
18	8 12 13	satffunlem2lem2	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) = ∅ )
19		funun	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) ∧ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) = ∅ ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) )
20	1 17 18 19	syl21anc	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) )
21		simpl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝑀 ∈ 𝑉 )
22		simpr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐸 ∈ 𝑊 )
23		simpl	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝑁 ∈ ω )
24	8 12 13	satfvsucsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) )
25	21 22 23 24	syl2an23an	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) )
26	25	funeqd	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ↔ Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) ) )
27	26	adantr	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ↔ Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) } ) ) )
28	20 27	mpbird	⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) )
29	28	ex	⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ) )

Metamath Proof Explorer

Theorem satffunlem2

Proof