satfsschain

Description: The binary relation of a satisfaction predicate as function over wff codes is an increasing chain (with respect to inclusion). (Contributed by AV, 15-Oct-2023)

		Ref	Expression
	Hypothesis	satfsschain.s	$⊢ S = M Sat E$
	Assertion	satfsschain	$⊢ ((M \in V \land E \in W) \land (A \in ω \land B \in ω)) \to (B \subseteq A \to S (B) \subseteq S (A))$

Proof

Step	Hyp	Ref	Expression
1		satfsschain.s	$⊢ S = M Sat E$
2		fveq2	$⊢ b = B \to S (b) = S (B)$
3	2	sseq2d	$⊢ b = B \to (S (B) \subseteq S (b) \leftrightarrow S (B) \subseteq S (B))$
4	3	imbi2d	$⊢ b = B \to (((M \in V \land E \in W) \to S (B) \subseteq S (b)) \leftrightarrow ((M \in V \land E \in W) \to S (B) \subseteq S (B)))$
5		fveq2	$⊢ b = a \to S (b) = S (a)$
6	5	sseq2d	$⊢ b = a \to (S (B) \subseteq S (b) \leftrightarrow S (B) \subseteq S (a))$
7	6	imbi2d	$⊢ b = a \to (((M \in V \land E \in W) \to S (B) \subseteq S (b)) \leftrightarrow ((M \in V \land E \in W) \to S (B) \subseteq S (a)))$
8		fveq2	$⊢ b = suc a \to S (b) = S (suc a)$
9	8	sseq2d	$⊢ b = suc a \to (S (B) \subseteq S (b) \leftrightarrow S (B) \subseteq S (suc a))$
10	9	imbi2d	$⊢ b = suc a \to (((M \in V \land E \in W) \to S (B) \subseteq S (b)) \leftrightarrow ((M \in V \land E \in W) \to S (B) \subseteq S (suc a)))$
11		fveq2	$⊢ b = A \to S (b) = S (A)$
12	11	sseq2d	$⊢ b = A \to (S (B) \subseteq S (b) \leftrightarrow S (B) \subseteq S (A))$
13	12	imbi2d	$⊢ b = A \to (((M \in V \land E \in W) \to S (B) \subseteq S (b)) \leftrightarrow ((M \in V \land E \in W) \to S (B) \subseteq S (A)))$
14		ssidd	$⊢ (M \in V \land E \in W) \to S (B) \subseteq S (B)$
15	14	a1i	$⊢ B \in ω \to ((M \in V \land E \in W) \to S (B) \subseteq S (B))$
16		pm2.27	$⊢ (M \in V \land E \in W) \to (((M \in V \land E \in W) \to S (B) \subseteq S (a)) \to S (B) \subseteq S (a))$
17	16	adantl	$⊢ (((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \to (((M \in V \land E \in W) \to S (B) \subseteq S (a)) \to S (B) \subseteq S (a))$
18		simpr	$⊢ ((((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \land S (B) \subseteq S (a)) \to S (B) \subseteq S (a)$
19		ssun1	$⊢ S (a) \subseteq S (a) \cup \{⟨x, y⟩ \| \exists u \in S (a) (\exists v \in S (a) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{z \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({z ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
20		simpl	$⊢ (M \in V \land E \in W) \to M \in V$
21		simpr	$⊢ (M \in V \land E \in W) \to E \in W$
22		simplll	$⊢ (((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \to a \in ω$
23	1	satfvsuc	$⊢ (M \in V \land E \in W \land a \in ω) \to S (suc a) = S (a) \cup \{⟨x, y⟩ \| \exists u \in S (a) (\exists v \in S (a) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{z \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({z ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
24	20 21 22 23	syl2an23an	$⊢ (((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \to S (suc a) = S (a) \cup \{⟨x, y⟩ \| \exists u \in S (a) (\exists v \in S (a) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{z \in (M^{ω}) \| \forall k \in M \{⟨i, k⟩\} \cup ({z ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
25	19 24	sseqtrrid	$⊢ (((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \to S (a) \subseteq S (suc a)$
26	25	adantr	$⊢ ((((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \land S (B) \subseteq S (a)) \to S (a) \subseteq S (suc a)$
27	18 26	sstrd	$⊢ ((((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \land S (B) \subseteq S (a)) \to S (B) \subseteq S (suc a)$
28	27	ex	$⊢ (((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \to (S (B) \subseteq S (a) \to S (B) \subseteq S (suc a))$
29	17 28	syld	$⊢ (((a \in ω \land B \in ω) \land B \subseteq a) \land (M \in V \land E \in W)) \to (((M \in V \land E \in W) \to S (B) \subseteq S (a)) \to S (B) \subseteq S (suc a))$
30	29	ex	$⊢ ((a \in ω \land B \in ω) \land B \subseteq a) \to ((M \in V \land E \in W) \to (((M \in V \land E \in W) \to S (B) \subseteq S (a)) \to S (B) \subseteq S (suc a)))$
31	30	com23	$⊢ ((a \in ω \land B \in ω) \land B \subseteq a) \to (((M \in V \land E \in W) \to S (B) \subseteq S (a)) \to ((M \in V \land E \in W) \to S (B) \subseteq S (suc a)))$
32	4 7 10 13 15 31	findsg	$⊢ ((A \in ω \land B \in ω) \land B \subseteq A) \to ((M \in V \land E \in W) \to S (B) \subseteq S (A))$
33	32	ex	$⊢ (A \in ω \land B \in ω) \to (B \subseteq A \to ((M \in V \land E \in W) \to S (B) \subseteq S (A)))$
34	33	com23	$⊢ (A \in ω \land B \in ω) \to ((M \in V \land E \in W) \to (B \subseteq A \to S (B) \subseteq S (A)))$
35	34	impcom	$⊢ ((M \in V \land E \in W) \land (A \in ω \land B \in ω)) \to (B \subseteq A \to S (B) \subseteq S (A))$

Metamath Proof Explorer

Theorem satfsschain

Proof