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	biimpi	$⊢ Fun S (suc N) \to Fun (M Sat E) (suc N)$
41	40	adantl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fun (M Sat E) (suc N)$
42	1	fveq1i	$⊢ S (N) = (M Sat E) (N)$
43	31 42 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)$
44	41 43	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))$
45	44	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))$
46		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))$
47	45 46	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))$
48	38 47	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))$
49	48	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)))$
50	4 42	difeq12i	$⊢ S (suc N) ∖ S (N) = (M Sat E) (suc N) ∖ (M Sat E) (N)$
51	50	eleq2i	$⊢ u \in (S (suc N) ∖ S (N)) \leftrightarrow u \in ((M Sat E) (suc N) ∖ (M Sat E) (N))$
52	51	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)))$
53	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)$
54		simpl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to N \in ω$
55	6 7 54	3jca	$⊢ (N \in ω \land (M \in V \land E \in W)) \to (M \in V \land E \in W \land N \in ω)$
56		satfdmfmla	$⊢ (M \in V \land E \in W \land N \in ω) \to dom (M Sat E) (N) = Fmla (N)$
57	55 56	syl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to dom (M Sat E) (N) = Fmla (N)$
58	57	eqcomd	$⊢ (N \in ω \land (M \in V \land E \in W)) \to Fmla (N) = dom (M Sat E) (N)$
59	58	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (N) = dom (M Sat E) (N)$
60	53 59	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)$
61	60	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)))$
62	49 52 61	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)))$
63	62	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))$
64	63	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))$
65		oveq1	$⊢ f = 1^{st} (u) \to f ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} g$
66	65	eqeq2d	$⊢ f = 1^{st} (u) \to (x = f ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} g)$
67	66	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)$
68		eqidd	$⊢ f = 1^{st} (u) \to i = i$
69		id	$⊢ f = 1^{st} (u) \to f = 1^{st} (u)$
70	68 69	goaleq12d	$⊢ f = 1^{st} (u) \to [\forall_{𝑔} i f] = [\forall_{𝑔} i 1^{st} (u)]$
71	70	eqeq2d	$⊢ f = 1^{st} (u) \to (x = [\forall_{𝑔} i f] \leftrightarrow x = [\forall_{𝑔} i 1^{st} (u)])$
72	71	rexbidv	$⊢ f = 1^{st} (u) \to (\exists i \in ω x = [\forall_{𝑔} i f] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
73	67 72	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)]))$
74	73	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)]))$
75	6	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to M \in V$
76	7	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to E \in W$
77	8	ad2antrr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to suc N \in ω$
78	75 76 77	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 ω)$
79		satfrel	$⊢ (M \in V \land E \in W \land suc N \in ω) \to Rel (M Sat E) (suc N)$
80	78 79	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel (M Sat E) (suc N)$
81	4	releqi	$⊢ Rel S (suc N) \leftrightarrow Rel (M Sat E) (suc N)$
82	80 81	sylibr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel S (suc N)$
83		1stdm	$⊢ (Rel S (suc N) \land v \in S (suc N)) \to 1^{st} (v) \in dom S (suc N)$
84	82 83	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)$
85	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)$
86	85	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)$
87	84 86	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)$
88	87	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)$
89		oveq2	$⊢ g = 1^{st} (v) \to 1^{st} (u) ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
90	89	eqeq2d	$⊢ g = 1^{st} (v) \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
91	90	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))$
92		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)$
93	88 91 92	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$
94	93	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)$
95	94	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)]))$
96	95	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)])$
97	64 74 96	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])$
98	97	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]))$
99	55	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 ω)$
100		satfrel	$⊢ (M \in V \land E \in W \land N \in ω) \to Rel (M Sat E) (N)$
101	99 100	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel (M Sat E) (N)$
102	42	releqi	$⊢ Rel S (N) \leftrightarrow Rel (M Sat E) (N)$
103	101 102	sylibr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel S (N)$
104		1stdm	$⊢ (Rel S (N) \land u \in S (N)) \to 1^{st} (u) \in dom S (N)$
105	103 104	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)$
106	42	dmeqi	$⊢ dom S (N) = dom (M Sat E) (N)$
107	99 56	syl	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom (M Sat E) (N) = Fmla (N)$
108	106 107	eqtrid	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to dom S (N) = Fmla (N)$
109	108	eqcomd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (N) = dom S (N)$
110	109	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)$
111	105 110	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)$
112	111	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)$
113	66	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)$
114	113	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)$
115		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))$
116		fveqeq2	$⊢ t = v \to (1^{st} (t) = 1^{st} (v) \leftrightarrow 1^{st} (v) = 1^{st} (v))$
117	116	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))$
118		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)$
119	115 117 118	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)$
120	44	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))$
121		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))$
122	120 121	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))$
123	119 122	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))$
124	123	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)))$
125	50	eleq2i	$⊢ v \in (S (suc N) ∖ S (N)) \leftrightarrow v \in ((M Sat E) (suc N) ∖ (M Sat E) (N))$
126	125	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)))$
127	12	eqcomd	$⊢ (N \in ω \land (M \in V \land E \in W)) \to Fmla (suc N) = dom (M Sat E) (suc N)$
128	127 58	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)$
129	128	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)))$
130	129	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)))$
131	124 126 130	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)))$
132	131	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)))$
133	132	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))$
134	133	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))$
135	90	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))$
136		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)$
137	134 135 136	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$
138	137	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$
139	112 114 138	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$
140	139	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)$
141	98 140	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))$
142	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 ω)$
143	11	eqcomd	$⊢ (M \in V \land E \in W \land suc N \in ω) \to Fmla (suc N) = dom (M Sat E) (suc N)$
144	142 143	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)$
145	107	eqcomd	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Fmla (N) = dom (M Sat E) (N)$
146	144 145	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)$
147	146	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)))$
148		eqid	$⊢ M Sat E = M Sat E$
149	148	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))$
150	28 29 149	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)$
151		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)$
152	80 150 151	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)$
153	147 152	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)$
154	50	eqcomi	$⊢ (M Sat E) (suc N) ∖ (M Sat E) (N) = S (suc N) ∖ S (N)$
155	154	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$
156		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]))$
157		oveq1	$⊢ 1^{st} (u) = f \to 1^{st} (u) ⊼_{𝑔} g = f ⊼_{𝑔} g$
158	157	eqeq2d	$⊢ 1^{st} (u) = f \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = f ⊼_{𝑔} g)$
159	158	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)$
160		eqidd	$⊢ 1^{st} (u) = f \to i = i$
161		id	$⊢ 1^{st} (u) = f \to 1^{st} (u) = f$
162	160 161	goaleq12d	$⊢ 1^{st} (u) = f \to [\forall_{𝑔} i 1^{st} (u)] = [\forall_{𝑔} i f]$
163	162	eqeq2d	$⊢ 1^{st} (u) = f \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow x = [\forall_{𝑔} i f])$
164	163	rexbidv	$⊢ 1^{st} (u) = f \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i f])$
165	159 164	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]))$
166	165	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]))$
167	142 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)$
168	167	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)$
169	168	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))$
170		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)$
171	80 170	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)$
172	169 171	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)$
173		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)$
174	1	eqcomi	$⊢ M Sat E = S$
175	174	fveq1i	$⊢ (M Sat E) (suc N) = S (suc N)$
176	175	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)$
177	89	eqcoms	$⊢ 1^{st} (v) = g \to 1^{st} (u) ⊼_{𝑔} g = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
178	177	eqeq2d	$⊢ 1^{st} (v) = g \to (x = 1^{st} (u) ⊼_{𝑔} g \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
179	178	biimpa	$⊢ (1^{st} (v) = g \land x = 1^{st} (u) ⊼_{𝑔} g) \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
180	179	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))$
181	180	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))$
182	176 181	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))$
183	173 182	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))$
184	183	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)))$
185	172 184	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)))$
186	185	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))$
187	186	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))$
188	187	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)]))$
189	166 188	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)]))$
190	189	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)]))$
191	190	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)]))$
192	156 191	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)]))$
193	192	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)])))$
194	155 193	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)])))$
195	153 194	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)])))$
196	195	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)]))$
197	145	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))$
198	55 100	syl	$⊢ (N \in ω \land (M \in V \land E \in W)) \to Rel (M Sat E) (N)$
199	198	adantr	$⊢ ((N \in ω \land (M \in V \land E \in W)) \land Fun S (suc N)) \to Rel (M Sat E) (N)$
200		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)$
201	199 200	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)$
202	197 201	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)$
203		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)$
204	42	eqcomi	$⊢ (M Sat E) (N) = S (N)$
205	204	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)$
206	158	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)$
207	206	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)$
208	146	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)))$
209		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)$
210	80 150 209	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)$
211	208 210	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)$
212	154	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$
213	178	biimpcd	$⊢ x = 1^{st} (u) ⊼_{𝑔} g \to (1^{st} (v) = g \to x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
214	213	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))$
215	214	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))$
216	215	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)))$
217	216	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)))$
218	212 217	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)))$
219	211 218	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)))$
220	219	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))$
221	220	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))$
222	207 221	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))$
223	222	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))$
224	223	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))$
225	205 224	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))$
226	203 225	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))$
227	226	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)))$
228	202 227	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)))$
229	228	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))$
230	196 229	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)))$
231	141 230	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))$
232	231	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)\}$
233	33 232	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)\}$
234	14 233	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)\}$
235		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$
236	235	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$
237	234 236	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