satffunlem2

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

		Ref	Expression
	Assertion	satffunlem2	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (Fun (M Sat E) (suc N) \to Fun (M Sat E) (suc suc N))$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun (M Sat E) (suc N)) \to Fun (M Sat E) (suc N)$
2		simpr	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (M \in V \land E \in W)$
3		peano2	$⊢ N \in ω \to suc N \in ω$
4	3	ancri	$⊢ N \in ω \to (suc N \in ω \land N \in ω)$
5	4	adantr	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (suc N \in ω \land N \in ω)$
6		sssucid	$⊢ N \subseteq suc N$
7	6	a1i	$⊢ (N \in ω \land (M \in V \land E \in W)) \to N \subseteq suc N$
8		eqid	$⊢ M Sat E = M Sat E$
9	8	satfsschain	$⊢ ((M \in V \land E \in W) \land (suc N \in ω \land N \in ω)) \to (N \subseteq suc N \to (M Sat E) (N) \subseteq (M Sat E) (suc N))$
10	9	imp	$⊢ (((M \in V \land E \in W) \land (suc N \in ω \land N \in ω)) \land N \subseteq suc N) \to (M Sat E) (N) \subseteq (M Sat E) (suc N)$
11	2 5 7 10	syl21anc	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (M Sat E) (N) \subseteq (M Sat E) (suc N)$
12		eqid	$⊢ (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
13		eqid	$⊢ \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
14	8 12 13	satffunlem2lem1	$⊢ (Fun (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N)) \to Fun \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\}$
15	14	expcom	$⊢ (M Sat E) (N) \subseteq (M Sat E) (suc N) \to (Fun (M Sat E) (suc N) \to Fun \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\})$
16	11 15	syl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (Fun (M Sat E) (suc N) \to Fun \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\})$
17	16	imp	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun (M Sat E) (suc N)) \to Fun \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\}$
18	8 12 13	satffunlem2lem2	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun (M Sat E) (suc N)) \to dom (M Sat E) (suc N) \cap dom \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\} = \emptyset$
19		funun	$⊢ ((Fun (M Sat E) (suc N) \land Fun \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\}) \land dom (M Sat E) (suc N) \cap dom \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\} = \emptyset) \to Fun ((M Sat E) (suc N) \cup \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\})$
20	1 17 18 19	syl21anc	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun (M Sat E) (suc N)) \to Fun ((M Sat E) (suc N) \cup \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\})$
21		simpl	$⊢ (M \in V \land E \in W) \to M \in V$
22		simpr	$⊢ (M \in V \land E \in W) \to E \in W$
23		simpl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to N \in ω$
24	8 12 13	satfvsucsuc	$⊢ (M \in V \land E \in W \land N \in ω) \to (M Sat E) (suc suc N) = (M Sat E) (suc N) \cup \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\}$
25	21 22 23 24	syl2an23an	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (M Sat E) (suc suc N) = (M Sat E) (suc N) \cup \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\}$
26	25	funeqd	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (Fun (M Sat E) (suc suc N) \leftrightarrow Fun ((M Sat E) (suc N) \cup \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\}))$
27	26	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun (M Sat E) (suc N)) \to (Fun (M Sat E) (suc suc N) \leftrightarrow Fun ((M Sat E) (suc N) \cup \{⟨x, y⟩ \| (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (\exists v \in (M Sat E) (suc N) (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 = \{f \in (M^{ω}) \| \forall j \in M \{⟨i, j⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \lor \exists u \in (M Sat E) (N) \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))\}))$
28	20 27	mpbird	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun (M Sat E) (suc N)) \to Fun (M Sat E) (suc suc N)$
29	28	ex	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (Fun (M Sat E) (suc N) \to Fun (M Sat E) (suc suc N))$

Metamath Proof Explorer

Theorem satffunlem2

Proof