Metamath Proof Explorer

Theorem satffunlem1

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

		Ref	Expression
	Assertion	satffunlem1	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		satfv0fun	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
2		satffunlem1lem1	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } )
3	1 2	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } )
4		satffunlem1lem2	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ∅ )
5		funun	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∧ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ∧ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ∅ ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
6	1 3 4 5	syl21anc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
7		peano1	⊢ ∅ ∈ ω
8		eqid	⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
9	8	satfvsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
10	7 9	mp3an3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
11	10	funeqd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) ↔ Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) )
12	6 11	mpbird	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) )