satfun

Description: The satisfaction predicate as function over wff codes in the model M and the binary relation E on M . (Contributed by AV, 29-Oct-2023)

		Ref	Expression
	Assertion	satfun	$⊢ (M \in V \land E \in W) \to (M Sat E) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω})$

Proof

Step	Hyp	Ref	Expression
1		satff	$⊢ (M \in V \land E \in W \land x \in ω) \to (M Sat E) (x) : Fmla (x) ⟶ 𝒫 (M^{ω})$
2	1	3expa	$⊢ ((M \in V \land E \in W) \land x \in ω) \to (M Sat E) (x) : Fmla (x) ⟶ 𝒫 (M^{ω})$
3		entric	$⊢ (x \in ω \land y \in ω) \to (x ≺ y \lor x \approx y \lor y ≺ x)$
4	3	adantl	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (x ≺ y \lor x \approx y \lor y ≺ x)$
5		nnsdomo	$⊢ (x \in ω \land y \in ω) \to (x ≺ y \leftrightarrow x \subset y)$
6	5	adantl	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (x ≺ y \leftrightarrow x \subset y)$
7		pm3.22	$⊢ (x \in ω \land y \in ω) \to (y \in ω \land x \in ω)$
8	7	anim2i	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to ((M \in V \land E \in W) \land (y \in ω \land x \in ω))$
9		pssss	$⊢ x \subset y \to x \subseteq y$
10		eqid	$⊢ M Sat E = M Sat E$
11	10	satfsschain	$⊢ ((M \in V \land E \in W) \land (y \in ω \land x \in ω)) \to (x \subseteq y \to (M Sat E) (x) \subseteq (M Sat E) (y))$
12	11	imp	$⊢ (((M \in V \land E \in W) \land (y \in ω \land x \in ω)) \land x \subseteq y) \to (M Sat E) (x) \subseteq (M Sat E) (y)$
13	8 9 12	syl2an	$⊢ (((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \land x \subset y) \to (M Sat E) (x) \subseteq (M Sat E) (y)$
14	13	orcd	$⊢ (((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \land x \subset y) \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x))$
15	14	ex	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (x \subset y \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
16	6 15	sylbid	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (x ≺ y \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
17		nneneq	$⊢ (x \in ω \land y \in ω) \to (x \approx y \leftrightarrow x = y)$
18	17	adantl	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (x \approx y \leftrightarrow x = y)$
19		ssid	$⊢ (M Sat E) (y) \subseteq (M Sat E) (y)$
20		fveq2	$⊢ x = y \to (M Sat E) (x) = (M Sat E) (y)$
21	19 20	sseqtrrid	$⊢ x = y \to (M Sat E) (y) \subseteq (M Sat E) (x)$
22	21	olcd	$⊢ x = y \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x))$
23	18 22	syl6bi	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (x \approx y \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
24		nnsdomo	$⊢ (y \in ω \land x \in ω) \to (y ≺ x \leftrightarrow y \subset x)$
25	24	ancoms	$⊢ (x \in ω \land y \in ω) \to (y ≺ x \leftrightarrow y \subset x)$
26	25	adantl	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (y ≺ x \leftrightarrow y \subset x)$
27	10	satfsschain	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (y \subseteq x \to (M Sat E) (y) \subseteq (M Sat E) (x))$
28		pssss	$⊢ y \subset x \to y \subseteq x$
29	27 28	impel	$⊢ (((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \land y \subset x) \to (M Sat E) (y) \subseteq (M Sat E) (x)$
30	29	olcd	$⊢ (((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \land y \subset x) \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x))$
31	30	ex	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (y \subset x \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
32	26 31	sylbid	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to (y ≺ x \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
33	16 23 32	3jaod	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to ((x ≺ y \lor x \approx y \lor y ≺ x) \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
34	4 33	mpd	$⊢ ((M \in V \land E \in W) \land (x \in ω \land y \in ω)) \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x))$
35	34	expr	$⊢ ((M \in V \land E \in W) \land x \in ω) \to (y \in ω \to ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
36	35	ralrimiv	$⊢ ((M \in V \land E \in W) \land x \in ω) \to \forall y \in ω ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x))$
37	2 36	jca	$⊢ ((M \in V \land E \in W) \land x \in ω) \to ((M Sat E) (x) : Fmla (x) ⟶ 𝒫 (M^{ω}) \land \forall y \in ω ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
38	37	ralrimiva	$⊢ (M \in V \land E \in W) \to \forall x \in ω ((M Sat E) (x) : Fmla (x) ⟶ 𝒫 (M^{ω}) \land \forall y \in ω ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x)))$
39		fvex	$⊢ (M Sat E) (x) \in V$
40	20 39	fiun	$⊢ \forall x \in ω ((M Sat E) (x) : Fmla (x) ⟶ 𝒫 (M^{ω}) \land \forall y \in ω ((M Sat E) (x) \subseteq (M Sat E) (y) \lor (M Sat E) (y) \subseteq (M Sat E) (x))) \to ⋃_{x \in ω} (M Sat E) (x) : ⋃_{x \in ω} Fmla (x) ⟶ 𝒫 (M^{ω})$
41	38 40	syl	$⊢ (M \in V \land E \in W) \to ⋃_{x \in ω} (M Sat E) (x) : ⋃_{x \in ω} Fmla (x) ⟶ 𝒫 (M^{ω})$
42		satom	$⊢ (M \in V \land E \in W) \to (M Sat E) (ω) = ⋃_{x \in ω} (M Sat E) (x)$
43		fmla	$⊢ Fmla (ω) = ⋃_{x \in ω} Fmla (x)$
44	43	a1i	$⊢ (M \in V \land E \in W) \to Fmla (ω) = ⋃_{x \in ω} Fmla (x)$
45	42 44	feq12d	$⊢ (M \in V \land E \in W) \to ((M Sat E) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω}) \leftrightarrow ⋃_{x \in ω} (M Sat E) (x) : ⋃_{x \in ω} Fmla (x) ⟶ 𝒫 (M^{ω}))$
46	41 45	mpbird	$⊢ (M \in V \land E \in W) \to (M Sat E) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω})$

Metamath Proof Explorer

Theorem satfun

Proof