Theorem satf0n0

Description: The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation does not contain the empty set. (Contributed by AV, 19-Sep-2023)

	Ref	Expression
Assertion	satf0n0	⊢ ( 𝑁 ∈ ω → ∅ ∉ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = ∅ → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ ∅ ) )
2	1	eleq2d	⊢ ( 𝑥 = ∅ → ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ) )
3	2	notbid	⊢ ( 𝑥 = ∅ → ( ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ) )
4		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) )
5	4	eleq2d	⊢ ( 𝑥 = 𝑦 → ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) )
6	5	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) )
7		fveq2	⊢ ( 𝑥 = suc 𝑦 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) )
8	7	eleq2d	⊢ ( 𝑥 = suc 𝑦 → ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) )
9	8	notbid	⊢ ( 𝑥 = suc 𝑦 → ( ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) )
10		fveq2	⊢ ( 𝑥 = 𝑁 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
11	10	eleq2d	⊢ ( 𝑥 = 𝑁 → ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
12	11	notbid	⊢ ( 𝑥 = 𝑁 → ( ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
13		0nelopab	⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) }
14		satf00	⊢ ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) }
15	14	eleq2i	⊢ ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ↔ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } )
16	13 15	mtbir	⊢ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ ∅ )
17		simpr	⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) → ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) )
18		0nelopab	⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) }
19		ioran	⊢ ( ¬ ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ∅ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ↔ ( ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∧ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) )
20	17 18 19	sylanblrc	⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) → ¬ ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ∅ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) )
21		eqid	⊢ ( ∅ Sat ∅ ) = ( ∅ Sat ∅ )
22	21	satf0suc	⊢ ( 𝑦 ∈ ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) )
23	22	adantr	⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) → ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) )
24	23	eleq2d	⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) → ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ↔ ∅ ∈ ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) )
25		elun	⊢ ( ∅ ∈ ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ↔ ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ∅ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) )
26	24 25	bitrdi	⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) → ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ↔ ( ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ ∅ ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) )
27	20 26	mtbird	⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) → ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) )
28	27	ex	⊢ ( 𝑦 ∈ ω → ( ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ) )
29	3 6 9 12 16 28	finds	⊢ ( 𝑁 ∈ ω → ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
30		df-nel	⊢ ( ∅ ∉ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ¬ ∅ ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
31	29 30	sylibr	⊢ ( 𝑁 ∈ ω → ∅ ∉ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )