satffunlem2lem2

	Ref	Expression
Hypotheses	satffunlem2lem2.s	$⊢ S = M Sat E$
	satffunlem2lem2.a	$⊢ A = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
	satffunlem2lem2.b	$⊢ B = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
Assertion	satffunlem2lem2	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom S (suc N) \cap dom \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		satffunlem2lem2.s	$⊢ S = M Sat E$
2		satffunlem2lem2.a	$⊢ A = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
3		satffunlem2lem2.b	$⊢ B = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
4	1	fveq1i	$⊢ S (suc N) = (M Sat E) (suc N)$
5	4	dmeqi	$⊢ dom S (suc N) = dom (M Sat E) (suc N)$
6		simprl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to M \in V$
7		simprr	$⊢ (N \in ω \land (M \in V \land E \in W)) \to E \in W$
8		peano2	$⊢ N \in ω \to suc N \in ω$
9	8	adantr	$⊢ (N \in ω \land (M \in V \land E \in W)) \to suc N \in ω$
10	6 7 9	3jca	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (M \in V \land E \in W \land suc N \in ω)$
11		satfdmfmla	$⊢ (M \in V \land E \in W \land suc N \in ω) \to dom (M Sat E) (suc N) = Fmla (suc N)$
12	10 11	syl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to dom (M Sat E) (suc N) = Fmla (suc N)$
13	12	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom (M Sat E) (suc N) = Fmla (suc N)$
14	5 13	eqtrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom S (suc N) = Fmla (suc N)$
15		ovex	$⊢ M^{ω} \in V$
16	15	difexi	$⊢ (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in V$
17	2 16	eqeltri	$⊢ A \in V$
18	17	a1i	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (suc N)) \land v \in S (suc N)) \to A \in V$
19	18	ralrimiva	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (suc N)) \to \forall v \in S (suc N) A \in V$
20	3 15	rabex2	$⊢ B \in V$
21	20	a1i	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (suc N)) \land i \in ω) \to B \in V$
22	21	ralrimiva	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (suc N)) \to \forall i \in ω B \in V$
23	19 22	jca	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (suc N)) \to (\forall v \in S (suc N) A \in V \land \forall i \in ω B \in V)$
24	23	ralrimiva	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to \forall u \in S (suc N) (\forall v \in S (suc N) A \in V \land \forall i \in ω B \in V)$
25		simplr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (M \in V \land E \in W)$
26	8	ancri	$⊢ N \in ω \to (suc N \in ω \land N \in ω)$
27	26	ad2antrr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (suc N \in ω \land N \in ω)$
28	25 27	jca	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((M \in V \land E \in W) \land (suc N \in ω \land N \in ω))$
29		sssucid	$⊢ N \subseteq suc N$
30	1	satfsschain	$⊢ ((M \in V \land E \in W) \land (suc N \in ω \land N \in ω)) \to (N \subseteq suc N \to S (N) \subseteq S (suc N))$
31	28 29 30	mpisyl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to S (N) \subseteq S (suc N)$
32		dmopab3rexdif	$⊢ (\forall u \in S (suc N) (\forall v \in S (suc N) A \in V \land \forall i \in ω B \in V) \land S (N) \subseteq S (suc N)) \to dom \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\} = \{x \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))\}$
33	24 31 32	syl2anc	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\} = \{x \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))\}$
34		simpr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))$
35		fveqeq2	$⊢ w = u \to (1^{st} (w) = 1^{st} (u) \leftrightarrow 1^{st} (u) = 1^{st} (u))$
36	35	adantl	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \land w = u) \to (1^{st} (w) = 1^{st} (u) \leftrightarrow 1^{st} (u) = 1^{st} (u))$
37		eqidd	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to 1^{st} (u) = 1^{st} (u)$
38	34 36 37	rspcedvd	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to \exists w \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (w) = 1^{st} (u)$
39	4	funeqi	$⊢ Fun S (suc N) \leftrightarrow Fun (M Sat E) (suc N)$
40	39	bilani	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fun (M Sat E) (suc N)$
41	1	fveq1i	$⊢ S (N) = (M Sat E) (N)$
42	31 41 4	3sstr3g	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (M Sat E) (N) \subseteq (M Sat E) (suc N)$
43	40 42	jca	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (Fun (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N))$
44	43	adantr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to (Fun (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N))$
45		funeldmdif	$⊢ (Fun (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N)) \to (1^{st} (u) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \leftrightarrow \exists w \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (w) = 1^{st} (u))$
46	44 45	syl	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to (1^{st} (u) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \leftrightarrow \exists w \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (w) = 1^{st} (u))$
47	38 46	mpbird	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to 1^{st} (u) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N))$
48	47	ex	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) \to 1^{st} (u) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)))$
49	4 41	difeq12i	$⊢ S (suc N) ∖ S (N) = (M Sat E) (suc N) ∖ (M Sat E) (N)$
50	49	eleq2i	$⊢ u \in (S (suc N) ∖ S (N)) \leftrightarrow u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))$
51	50	a1i	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (u \in (S (suc N) ∖ S (N)) \leftrightarrow u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)))$
52	13	eqcomd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (suc N) = dom (M Sat E) (suc N)$
53		simpl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to N \in ω$
54	6 7 53	3jca	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (M \in V \land E \in W \land N \in ω)$
55		satfdmfmla	$⊢ (M \in V \land E \in W \land N \in ω) \to dom (M Sat E) (N) = Fmla (N)$
56	54 55	syl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to dom (M Sat E) (N) = Fmla (N)$
57	56	eqcomd	$⊢ (N \in ω \land (M \in V \land E \in W)) \to Fmla (N) = dom (M Sat E) (N)$
58	57	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (N) = dom (M Sat E) (N)$
59	52 58	difeq12d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (suc N) ∖ Fmla (N) = dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)$
60	59	eleq2d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (1^{st} (u) \in (Fmla (suc N) ∖ Fmla (N)) \leftrightarrow 1^{st} (u) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)))$
61	48 51 60	3imtr4d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (u \in (S (suc N) ∖ S (N)) \to 1^{st} (u) \in (Fmla (suc N) ∖ Fmla (N)))$
62	61	imp	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to 1^{st} (u) \in (Fmla (suc N) ∖ Fmla (N))$
63	62	adantr	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to 1^{st} (u) \in (Fmla (suc N) ∖ Fmla (N))$
64		oveq1	$⊢ f = 1^{st} (u) \to f ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} g$
65	64	eqeq2d	$⊢ f = 1^{st} (u) \to (x = f ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} g)$
66	65	rexbidv	$⊢ f = 1^{st} (u) \to (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \leftrightarrow \exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g)$
67		eqidd	$⊢ f = 1^{st} (u) \to i = i$
68		id	$⊢ f = 1^{st} (u) \to f = 1^{st} (u)$
69	67 68	goaleq12d	$⊢ f = 1^{st} (u) \to [\forall_{𝑔} i f] = [\forall_{𝑔} i 1^{st} (u)]$
70	69	eqeq2d	$⊢ f = 1^{st} (u) \to (x = [\forall_{𝑔} i f] \leftrightarrow x = [\forall_{𝑔} i 1^{st} (u)])$
71	70	rexbidv	$⊢ f = 1^{st} (u) \to (\exists i \in ω x = [\forall_{𝑔} i f] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
72	66 71	orbi12d	$⊢ f = 1^{st} (u) \to ((\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \leftrightarrow (\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
73	72	adantl	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \land f = 1^{st} (u)) \to ((\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \leftrightarrow (\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
74	6	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to M \in V$
75	7	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to E \in W$
76	8	ad2antrr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to suc N \in ω$
77	74 75 76	3jca	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (M \in V \land E \in W \land suc N \in ω)$
78		satfrel	$⊢ (M \in V \land E \in W \land suc N \in ω) \to Rel (M Sat E) (suc N)$
79	77 78	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel (M Sat E) (suc N)$
80	4	releqi	$⊢ Rel S (suc N) \leftrightarrow Rel (M Sat E) (suc N)$
81	79 80	sylibr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel S (suc N)$
82		1stdm	$⊢ (Rel S (suc N) \land v \in S (suc N)) \to 1^{st} (v) \in dom S (suc N)$
83	81 82	sylan	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in S (suc N)) \to 1^{st} (v) \in dom S (suc N)$
84	14	eqcomd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (suc N) = dom S (suc N)$
85	84	adantr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in S (suc N)) \to Fmla (suc N) = dom S (suc N)$
86	83 85	eleqtrrd	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in S (suc N)) \to 1^{st} (v) \in Fmla (suc N)$
87	86	ad4ant13	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to 1^{st} (v) \in Fmla (suc N)$
88		oveq2	$⊢ g = 1^{st} (v) \to 1^{st} (u) ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
89	88	eqeq2d	$⊢ g = 1^{st} (v) \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
90	89	adantl	$⊢ ((((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \land g = 1^{st} (v)) \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
91		simpr	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
92	87 90 91	rspcedvd	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land v \in S (suc N)) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to \exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g$
93	92	rexlimdva2	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g)$
94	93	orim1d	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to ((\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to (\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
95	94	imp	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to (\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
96	63 73 95	rspcedvd	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \to \exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])$
97	96	rexlimdva2	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to \exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
98	54	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (M \in V \land E \in W \land N \in ω)$
99		satfrel	$⊢ (M \in V \land E \in W \land N \in ω) \to Rel (M Sat E) (N)$
100	98 99	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel (M Sat E) (N)$
101	41	releqi	$⊢ Rel S (N) \leftrightarrow Rel (M Sat E) (N)$
102	100 101	sylibr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel S (N)$
103		1stdm	$⊢ (Rel S (N) \land u \in S (N)) \to 1^{st} (u) \in dom S (N)$
104	102 103	sylan	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \to 1^{st} (u) \in dom S (N)$
105	41	dmeqi	$⊢ dom S (N) = dom (M Sat E) (N)$
106	98 55	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom (M Sat E) (N) = Fmla (N)$
107	105 106	eqtrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom S (N) = Fmla (N)$
108	107	eqcomd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (N) = dom S (N)$
109	108	adantr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \to Fmla (N) = dom S (N)$
110	104 109	eleqtrrd	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \to 1^{st} (u) \in Fmla (N)$
111	110	adantr	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to 1^{st} (u) \in Fmla (N)$
112	65	rexbidv	$⊢ f = 1^{st} (u) \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g \leftrightarrow \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g)$
113	112	adantl	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \land f = 1^{st} (u)) \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g \leftrightarrow \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g)$
114		simpr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))$
115		fveqeq2	$⊢ t = v \to (1^{st} (t) = 1^{st} (v) \leftrightarrow 1^{st} (v) = 1^{st} (v))$
116	115	adantl	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \land t = v) \to (1^{st} (t) = 1^{st} (v) \leftrightarrow 1^{st} (v) = 1^{st} (v))$
117		eqidd	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to 1^{st} (v) = 1^{st} (v)$
118	114 116 117	rspcedvd	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to \exists t \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (t) = 1^{st} (v)$
119	43	adantr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to (Fun (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N))$
120		funeldmdif	$⊢ (Fun (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N)) \to (1^{st} (v) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \leftrightarrow \exists t \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (t) = 1^{st} (v))$
121	119 120	syl	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to (1^{st} (v) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \leftrightarrow \exists t \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (t) = 1^{st} (v))$
122	118 121	mpbird	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))) \to 1^{st} (v) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N))$
123	122	ex	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) \to 1^{st} (v) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)))$
124	49	eleq2i	$⊢ v \in (S (suc N) ∖ S (N)) \leftrightarrow v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))$
125	124	a1i	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (v \in (S (suc N) ∖ S (N)) \leftrightarrow v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)))$
126	12	eqcomd	$⊢ (N \in ω \land (M \in V \land E \in W)) \to Fmla (suc N) = dom (M Sat E) (suc N)$
127	126 57	difeq12d	$⊢ (N \in ω \land (M \in V \land E \in W)) \to Fmla (suc N) ∖ Fmla (N) = dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)$
128	127	eleq2d	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (1^{st} (v) \in (Fmla (suc N) ∖ Fmla (N)) \leftrightarrow 1^{st} (v) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)))$
129	128	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (1^{st} (v) \in (Fmla (suc N) ∖ Fmla (N)) \leftrightarrow 1^{st} (v) \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)))$
130	123 125 129	3imtr4d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (v \in (S (suc N) ∖ S (N)) \to 1^{st} (v) \in (Fmla (suc N) ∖ Fmla (N)))$
131	130	adantr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \to (v \in (S (suc N) ∖ S (N)) \to 1^{st} (v) \in (Fmla (suc N) ∖ Fmla (N)))$
132	131	imp	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land v \in (S (suc N) ∖ S (N))) \to 1^{st} (v) \in (Fmla (suc N) ∖ Fmla (N))$
133	132	adantr	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land v \in (S (suc N) ∖ S (N))) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to 1^{st} (v) \in (Fmla (suc N) ∖ Fmla (N))$
134	89	adantl	$⊢ ((((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land v \in (S (suc N) ∖ S (N))) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \land g = 1^{st} (v)) \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
135		simpr	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land v \in (S (suc N) ∖ S (N))) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
136	133 134 135	rspcedvd	$⊢ (((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land v \in (S (suc N) ∖ S (N))) \land x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g$
137	136	r19.29an	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g$
138	111 113 137	rspcedvd	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in S (N)) \land \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g$
139	138	rexlimdva2	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)$
140	97 139	orim12d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \to (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g))$
141	10	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (M \in V \land E \in W \land suc N \in ω)$
142	11	eqcomd	$⊢ (M \in V \land E \in W \land suc N \in ω) \to Fmla (suc N) = dom (M Sat E) (suc N)$
143	141 142	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (suc N) = dom (M Sat E) (suc N)$
144	106	eqcomd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (N) = dom (M Sat E) (N)$
145	143 144	difeq12d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (suc N) ∖ Fmla (N) = dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)$
146	145	eleq2d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in (Fmla (suc N) ∖ Fmla (N)) \leftrightarrow f \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)))$
147		eqid	$⊢ M Sat E = M Sat E$
148	147	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))$
149	28 29 148	mpisyl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (M Sat E) (N) \subseteq (M Sat E) (suc N)$
150		releldmdifi	$⊢ (Rel (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N)) \to (f \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \to \exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (u) = f)$
151	79 149 150	syl2anc	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \to \exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (u) = f)$
152	146 151	sylbid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in (Fmla (suc N) ∖ Fmla (N)) \to \exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (u) = f)$
153	49	eqcomi	$⊢ (M Sat E) (suc N) ∖ (M Sat E) (N) = S (suc N) ∖ S (N)$
154	153	rexeqi	$⊢ \exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (u) = f \leftrightarrow \exists u \in (S (suc N) ∖ S (N)) 1^{st} (u) = f$
155		r19.41v	$⊢ \exists u \in (S (suc N) ∖ S (N)) (1^{st} (u) = f \land (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \leftrightarrow (\exists u \in (S (suc N) ∖ S (N)) 1^{st} (u) = f \land (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
156		oveq1	$⊢ 1^{st} (u) = f \to 1^{st} (u) ⊼_{𝑔} g = f ⊼_{𝑔} g$
157	156	eqeq2d	$⊢ 1^{st} (u) = f \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = f ⊼_{𝑔} g)$
158	157	rexbidv	$⊢ 1^{st} (u) = f \to (\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow \exists g \in Fmla (suc N) x = f ⊼_{𝑔} g)$
159		eqidd	$⊢ 1^{st} (u) = f \to i = i$
160		id	$⊢ 1^{st} (u) = f \to 1^{st} (u) = f$
161	159 160	goaleq12d	$⊢ 1^{st} (u) = f \to [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} i f]$
162	161	eqeq2d	$⊢ 1^{st} (u) = f \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow x = [\forall_{𝑔} i f])$
163	162	rexbidv	$⊢ 1^{st} (u) = f \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i f])$
164	158 163	orbi12d	$⊢ 1^{st} (u) = f \to ((\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
165	164	adantl	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land 1^{st} (u) = f) \to ((\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]))$
166	141 11	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom (M Sat E) (suc N) = Fmla (suc N)$
167	166	eqcomd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (suc N) = dom (M Sat E) (suc N)$
168	167	eleq2d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in Fmla (suc N) \leftrightarrow g \in dom (M Sat E) (suc N))$
169		releldm2	$⊢ Rel (M Sat E) (suc N) \to (g \in dom (M Sat E) (suc N) \leftrightarrow \exists v \in (M Sat E) (suc N) 1^{st} (v) = g)$
170	79 169	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in dom (M Sat E) (suc N) \leftrightarrow \exists v \in (M Sat E) (suc N) 1^{st} (v) = g)$
171	168 170	bitrd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in Fmla (suc N) \leftrightarrow \exists v \in (M Sat E) (suc N) 1^{st} (v) = g)$
172		r19.41v	$⊢ \exists v \in (M Sat E) (suc N) (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \leftrightarrow (\exists v \in (M Sat E) (suc N) 1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g)$
173	1	eqcomi	$⊢ M Sat E = S$
174	173	fveq1i	$⊢ (M Sat E) (suc N) = S (suc N)$
175	174	rexeqi	$⊢ \exists v \in (M Sat E) (suc N) (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \leftrightarrow \exists v \in S (suc N) (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g)$
176	88	eqcoms	$⊢ 1^{st} (v) = g \to 1^{st} (u) ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
177	176	eqeq2d	$⊢ 1^{st} (v) = g \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
178	177	biimpa	$⊢ (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
179	178	a1i	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
180	179	reximdv	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists v \in S (suc N) (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to \exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
181	175 180	biimtrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists v \in (M Sat E) (suc N) (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to \exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
182	172 181	biimtrrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((\exists v \in (M Sat E) (suc N) 1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to \exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
183	182	expd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists v \in (M Sat E) (suc N) 1^{st} (v) = g \to (x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
184	171 183	sylbid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in Fmla (suc N) \to (x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
185	184	rexlimdv	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
186	185	ad2antrr	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land 1^{st} (u) = f) \to (\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
187	186	orim1d	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land 1^{st} (u) = f) \to ((\exists g \in Fmla (suc N) x = 1^{st} (u) ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \to (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
188	165 187	sylbird	$⊢ ((((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \land 1^{st} (u) = f) \to ((\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
189	188	expimpd	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land u \in (S (suc N) ∖ S (N))) \to ((1^{st} (u) = f \land (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \to (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
190	189	reximdva	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in (S (suc N) ∖ S (N)) (1^{st} (u) = f \land (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \to \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
191	155 190	biimtrrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((\exists u \in (S (suc N) ∖ S (N)) 1^{st} (u) = f \land (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f])) \to \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
192	191	expd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in (S (suc N) ∖ S (N)) 1^{st} (u) = f \to ((\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
193	154 192	biimtrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (u) = f \to ((\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
194	152 193	syld	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in (Fmla (suc N) ∖ Fmla (N)) \to ((\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
195	194	rexlimdv	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \to \exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
196	144	eleq2d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in Fmla (N) \leftrightarrow f \in dom (M Sat E) (N))$
197	54 99	syl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to Rel (M Sat E) (N)$
198	197	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel (M Sat E) (N)$
199		releldm2	$⊢ Rel (M Sat E) (N) \to (f \in dom (M Sat E) (N) \leftrightarrow \exists u \in (M Sat E) (N) 1^{st} (u) = f)$
200	198 199	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in dom (M Sat E) (N) \leftrightarrow \exists u \in (M Sat E) (N) 1^{st} (u) = f)$
201	196 200	bitrd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in Fmla (N) \leftrightarrow \exists u \in (M Sat E) (N) 1^{st} (u) = f)$
202		r19.41v	$⊢ \exists u \in (M Sat E) (N) (1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g) \leftrightarrow (\exists u \in (M Sat E) (N) 1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)$
203	41	eqcomi	$⊢ (M Sat E) (N) = S (N)$
204	203	rexeqi	$⊢ \exists u \in (M Sat E) (N) (1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g) \leftrightarrow \exists u \in S (N) (1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)$
205	157	rexbidv	$⊢ 1^{st} (u) = f \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)$
206	205	adantl	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land 1^{st} (u) = f) \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)$
207	145	eleq2d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in (Fmla (suc N) ∖ Fmla (N)) \leftrightarrow g \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)))$
208		releldmdifi	$⊢ (Rel (M Sat E) (suc N) \land (M Sat E) (N) \subseteq (M Sat E) (suc N)) \to (g \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \to \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (v) = g)$
209	79 149 208	syl2anc	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in (dom (M Sat E) (suc N) ∖ dom (M Sat E) (N)) \to \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (v) = g)$
210	207 209	sylbid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in (Fmla (suc N) ∖ Fmla (N)) \to \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (v) = g)$
211	153	rexeqi	$⊢ \exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (v) = g \leftrightarrow \exists v \in (S (suc N) ∖ S (N)) 1^{st} (v) = g$
212	177	biimpcd	$⊢ x = 1^{st} (u) ⊼_{𝑔} g \to (1^{st} (v) = g \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
213	212	adantl	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land x = 1^{st} (u) ⊼_{𝑔} g) \to (1^{st} (v) = g \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
214	213	reximdv	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land x = 1^{st} (u) ⊼_{𝑔} g) \to (\exists v \in (S (suc N) ∖ S (N)) 1^{st} (v) = g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
215	214	ex	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (x = 1^{st} (u) ⊼_{𝑔} g \to (\exists v \in (S (suc N) ∖ S (N)) 1^{st} (v) = g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
216	215	com23	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists v \in (S (suc N) ∖ S (N)) 1^{st} (v) = g \to (x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
217	211 216	biimtrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists v \in ((M Sat E) (suc N) ∖ (M Sat E) (N)) 1^{st} (v) = g \to (x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
218	210 217	syld	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (g \in (Fmla (suc N) ∖ Fmla (N)) \to (x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
219	218	rexlimdv	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
220	219	adantr	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land 1^{st} (u) = f) \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = 1^{st} (u) ⊼_{𝑔} g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
221	206 220	sylbird	$⊢ (((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \land 1^{st} (u) = f) \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
222	221	expimpd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g) \to \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
223	222	reximdv	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in S (N) (1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g) \to \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
224	204 223	biimtrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in (M Sat E) (N) (1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g) \to \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
225	202 224	biimtrrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((\exists u \in (M Sat E) (N) 1^{st} (u) = f \land \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g) \to \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
226	225	expd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists u \in (M Sat E) (N) 1^{st} (u) = f \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g \to \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
227	201 226	sylbid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (f \in Fmla (N) \to (\exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g \to \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
228	227	rexlimdv	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to (\exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g \to \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
229	195 228	orim12d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g) \to (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)))$
230	140 229	impbid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to ((\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)) \leftrightarrow (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g))$
231	230	abbidv	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to \{x \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))\} = \{x \| (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)\}$
232	33 231	eqtrd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\} = \{x \| (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)\}$
233	14 232	ineq12d	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom S (suc N) \cap dom \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\} = Fmla (suc N) \cap \{x \| (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)\}$
234		fmlasucdisj	$⊢ N \in ω \to Fmla (suc N) \cap \{x \| (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)\} = \emptyset$
235	234	ad2antrr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (suc N) \cap \{x \| (\exists f \in (Fmla (suc N) ∖ Fmla (N)) (\exists g \in Fmla (suc N) x = f ⊼_{𝑔} g \lor \exists i \in ω x = [\forall_{𝑔} i f]) \lor \exists f \in Fmla (N) \exists g \in (Fmla (suc N) ∖ Fmla (N)) x = f ⊼_{𝑔} g)\} = \emptyset$
236	233 235	eqtrd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom S (suc N) \cap dom \{⟨x, y⟩ \| (\exists u \in (S (suc N) ∖ S (N)) (\exists v \in S (suc N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = B)) \lor \exists u \in S (N) \exists v \in (S (suc N) ∖ S (N)) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = A))\} = \emptyset$

Metamath Proof Explorer

Theorem satffunlem2lem2

Proof