sat1el2xp

Description: The first component of an element of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation is a member of a doubled Cartesian product. (Contributed by AV, 17-Sep-2023)

		Ref	Expression
	Assertion	sat1el2xp	$⊢ N \in ω \to \forall w \in (\emptyset Sat \emptyset) (N) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = \emptyset \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (\emptyset)$
2	1	raleqdv	$⊢ x = \emptyset \to (\forall w \in (\emptyset Sat \emptyset) (x) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \forall w \in (\emptyset Sat \emptyset) (\emptyset) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)))$
3		fveq2	$⊢ x = y \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (y)$
4	3	raleqdv	$⊢ x = y \to (\forall w \in (\emptyset Sat \emptyset) (x) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)))$
5		fveq2	$⊢ x = suc y \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (suc y)$
6	5	raleqdv	$⊢ x = suc y \to (\forall w \in (\emptyset Sat \emptyset) (x) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \forall w \in (\emptyset Sat \emptyset) (suc y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)))$
7		fveq2	$⊢ x = N \to (\emptyset Sat \emptyset) (x) = (\emptyset Sat \emptyset) (N)$
8	7	raleqdv	$⊢ x = N \to (\forall w \in (\emptyset Sat \emptyset) (x) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \forall w \in (\emptyset Sat \emptyset) (N) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)))$
9		eqeq1	$⊢ x = 1^{st} (w) \to (x = i \in_{𝑔} j \leftrightarrow 1^{st} (w) = i \in_{𝑔} j)$
10	9	2rexbidv	$⊢ x = 1^{st} (w) \to (\exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω 1^{st} (w) = i \in_{𝑔} j)$
11	10	anbi2d	$⊢ x = 1^{st} (w) \to ((z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \leftrightarrow (z = \emptyset \land \exists i \in ω \exists j \in ω 1^{st} (w) = i \in_{𝑔} j))$
12		eqeq1	$⊢ z = 2^{nd} (w) \to (z = \emptyset \leftrightarrow 2^{nd} (w) = \emptyset)$
13	12	anbi1d	$⊢ z = 2^{nd} (w) \to ((z = \emptyset \land \exists i \in ω \exists j \in ω 1^{st} (w) = i \in_{𝑔} j) \leftrightarrow (2^{nd} (w) = \emptyset \land \exists i \in ω \exists j \in ω 1^{st} (w) = i \in_{𝑔} j))$
14	11 13	elopabi	$⊢ w \in \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} \to (2^{nd} (w) = \emptyset \land \exists i \in ω \exists j \in ω 1^{st} (w) = i \in_{𝑔} j)$
15		goel	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j = ⟨\emptyset, ⟨i, j⟩⟩$
16	15	eqeq2d	$⊢ (i \in ω \land j \in ω) \to (1^{st} (w) = i \in_{𝑔} j \leftrightarrow 1^{st} (w) = ⟨\emptyset, ⟨i, j⟩⟩)$
17		omex	$⊢ ω \in V$
18	17 17	pm3.2i	$⊢ (ω \in V \land ω \in V)$
19		peano1	$⊢ \emptyset \in ω$
20	19	a1i	$⊢ (i \in ω \land j \in ω) \to \emptyset \in ω$
21		opelxpi	$⊢ (i \in ω \land j \in ω) \to ⟨i, j⟩ \in (ω \times ω)$
22	20 21	opelxpd	$⊢ (i \in ω \land j \in ω) \to ⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (ω \times ω))$
23		xpeq12	$⊢ (a = ω \land b = ω) \to a \times b = ω \times ω$
24	23	xpeq2d	$⊢ (a = ω \land b = ω) \to ω \times (a \times b) = ω \times (ω \times ω)$
25	24	eleq2d	$⊢ (a = ω \land b = ω) \to (⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (a \times b)) \leftrightarrow ⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (ω \times ω)))$
26	25	spc2egv	$⊢ (ω \in V \land ω \in V) \to (⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (ω \times ω)) \to \exists a \exists b ⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (a \times b)))$
27	18 22 26	mpsyl	$⊢ (i \in ω \land j \in ω) \to \exists a \exists b ⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (a \times b))$
28		eleq1	$⊢ 1^{st} (w) = ⟨\emptyset, ⟨i, j⟩⟩ \to (1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow ⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (a \times b)))$
29	28	2exbidv	$⊢ 1^{st} (w) = ⟨\emptyset, ⟨i, j⟩⟩ \to (\exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \exists a \exists b ⟨\emptyset, ⟨i, j⟩⟩ \in (ω \times (a \times b)))$
30	27 29	syl5ibrcom	$⊢ (i \in ω \land j \in ω) \to (1^{st} (w) = ⟨\emptyset, ⟨i, j⟩⟩ \to \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)))$
31	16 30	sylbid	$⊢ (i \in ω \land j \in ω) \to (1^{st} (w) = i \in_{𝑔} j \to \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)))$
32	31	rexlimivv	$⊢ \exists i \in ω \exists j \in ω 1^{st} (w) = i \in_{𝑔} j \to \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))$
33	32	adantl	$⊢ (2^{nd} (w) = \emptyset \land \exists i \in ω \exists j \in ω 1^{st} (w) = i \in_{𝑔} j) \to \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))$
34	14 33	syl	$⊢ w \in \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} \to \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))$
35		satf00	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
36	34 35	eleq2s	$⊢ w \in (\emptyset Sat \emptyset) (\emptyset) \to \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))$
37	36	rgen	$⊢ \forall w \in (\emptyset Sat \emptyset) (\emptyset) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))$
38		omsucelsucb	$⊢ y \in ω \leftrightarrow suc y \in suc ω$
39		satf0sucom	$⊢ suc y \in suc ω \to (\emptyset Sat \emptyset) (suc y) = rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc y)$
40	38 39	sylbi	$⊢ y \in ω \to (\emptyset Sat \emptyset) (suc y) = rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc y)$
41	40	adantr	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (\emptyset Sat \emptyset) (suc y) = rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc y)$
42		nnon	$⊢ y \in ω \to y \in On$
43		rdgsuc	$⊢ y \in On \to rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc y) = (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y))$
44	42 43	syl	$⊢ y \in ω \to rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc y) = (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y))$
45	44	adantr	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc y) = (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y))$
46		elelsuc	$⊢ y \in ω \to y \in suc ω$
47		satf0sucom	$⊢ y \in suc ω \to (\emptyset Sat \emptyset) (y) = rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y)$
48	46 47	syl	$⊢ y \in ω \to (\emptyset Sat \emptyset) (y) = rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y)$
49	48	eqcomd	$⊢ y \in ω \to rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y) = (\emptyset Sat \emptyset) (y)$
50	49	fveq2d	$⊢ y \in ω \to (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y)) = (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) ((\emptyset Sat \emptyset) (y))$
51	50	adantr	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) (rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (y)) = (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) ((\emptyset Sat \emptyset) (y))$
52		eqidd	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) = (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\})$
53		id	$⊢ f = (\emptyset Sat \emptyset) (y) \to f = (\emptyset Sat \emptyset) (y)$
54		rexeq	$⊢ f = (\emptyset Sat \emptyset) (y) \to (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow \exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
55	54	orbi1d	$⊢ f = (\emptyset Sat \emptyset) (y) \to ((\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
56	55	rexeqbi1dv	$⊢ f = (\emptyset Sat \emptyset) (y) \to (\exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
57	56	anbi2d	$⊢ f = (\emptyset Sat \emptyset) (y) \to ((z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
58	57	opabbidv	$⊢ f = (\emptyset Sat \emptyset) (y) \to \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
59	53 58	uneq12d	$⊢ f = (\emptyset Sat \emptyset) (y) \to f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
60	59	adantl	$⊢ ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \land f = (\emptyset Sat \emptyset) (y)) \to f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} = (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
61		fvexd	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (\emptyset Sat \emptyset) (y) \in V$
62	17	a1i	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to ω \in V$
63		satf0suclem	$⊢ ((\emptyset Sat \emptyset) (y) \in V \land (\emptyset Sat \emptyset) (y) \in V \land ω \in V) \to \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
64	61 61 62 63	syl3anc	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
65		unexg	$⊢ ((\emptyset Sat \emptyset) (y) \in V \land \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V) \to (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
66	61 64 65	syl2anc	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \in V$
67	52 60 61 66	fvmptd	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) ((\emptyset Sat \emptyset) (y)) = (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
68	45 51 67	3eqtrd	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to rec ((f \in V ⟼ f \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (suc y) = (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
69	41 68	eqtrd	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (\emptyset Sat \emptyset) (suc y) = (\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}$
70	69	eleq2d	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (t \in (\emptyset Sat \emptyset) (suc y) \leftrightarrow t \in ((\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}))$
71		elun	$⊢ t \in ((\emptyset Sat \emptyset) (y) \cup \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (t \in (\emptyset Sat \emptyset) (y) \lor t \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\})$
72	70 71	bitrdi	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (t \in (\emptyset Sat \emptyset) (suc y) \leftrightarrow (t \in (\emptyset Sat \emptyset) (y) \lor t \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}))$
73		fveq2	$⊢ w = t \to 1^{st} (w) = 1^{st} (t)$
74	73	eleq1d	$⊢ w = t \to (1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow 1^{st} (t) \in (ω \times (a \times b)))$
75	74	2exbidv	$⊢ w = t \to (\exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
76	75	rspccv	$⊢ \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to (t \in (\emptyset Sat \emptyset) (y) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
77	76	adantl	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (t \in (\emptyset Sat \emptyset) (y) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
78		fveq2	$⊢ w = v \to 1^{st} (w) = 1^{st} (v)$
79	78	eleq1d	$⊢ w = v \to (1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow 1^{st} (v) \in (ω \times (a \times b)))$
80	79	2exbidv	$⊢ w = v \to (\exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \exists a \exists b 1^{st} (v) \in (ω \times (a \times b)))$
81	80	rspcva	$⊢ (v \in (\emptyset Sat \emptyset) (y) \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (v) \in (ω \times (a \times b))$
82		sels	$⊢ 1^{st} (v) \in (ω \times (a \times b)) \to \exists s 1^{st} (v) \in s$
83	82	exlimivv	$⊢ \exists a \exists b 1^{st} (v) \in (ω \times (a \times b)) \to \exists s 1^{st} (v) \in s$
84	81 83	syl	$⊢ (v \in (\emptyset Sat \emptyset) (y) \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists s 1^{st} (v) \in s$
85	84	expcom	$⊢ \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to (v \in (\emptyset Sat \emptyset) (y) \to \exists s 1^{st} (v) \in s)$
86		fveq2	$⊢ w = u \to 1^{st} (w) = 1^{st} (u)$
87	86	eleq1d	$⊢ w = u \to (1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow 1^{st} (u) \in (ω \times (a \times b)))$
88	87	2exbidv	$⊢ w = u \to (\exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \exists a \exists b 1^{st} (u) \in (ω \times (a \times b)))$
89	88	rspcva	$⊢ (u \in (\emptyset Sat \emptyset) (y) \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (u) \in (ω \times (a \times b))$
90		sels	$⊢ 1^{st} (u) \in (ω \times (a \times b)) \to \exists s 1^{st} (u) \in s$
91	90	exlimivv	$⊢ \exists a \exists b 1^{st} (u) \in (ω \times (a \times b)) \to \exists s 1^{st} (u) \in s$
92	89 91	syl	$⊢ (u \in (\emptyset Sat \emptyset) (y) \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists s 1^{st} (u) \in s$
93		eleq2w	$⊢ s = r \to (1^{st} (u) \in s \leftrightarrow 1^{st} (u) \in r)$
94	93	cbvexvw	$⊢ \exists s 1^{st} (u) \in s \leftrightarrow \exists r 1^{st} (u) \in r$
95		vex	$⊢ r \in V$
96		vex	$⊢ s \in V$
97	95 96	pm3.2i	$⊢ (r \in V \land s \in V)$
98		df-ov	$⊢ 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = ⊼_{𝑔} (⟨1^{st} (u), 1^{st} (v)⟩)$
99		df-gona	$⊢ ⊼_{𝑔} = (e \in (V \times V) ⟼ ⟨1_{𝑜}, e⟩)$
100		opeq2	$⊢ e = ⟨1^{st} (u), 1^{st} (v)⟩ \to ⟨1_{𝑜}, e⟩ = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
101		opelvvg	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to ⟨1^{st} (u), 1^{st} (v)⟩ \in (V \times V)$
102		opex	$⊢ ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ \in V$
103	102	a1i	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ \in V$
104	99 100 101 103	fvmptd3	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to ⊼_{𝑔} (⟨1^{st} (u), 1^{st} (v)⟩) = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
105	98 104	eqtrid	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) = ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩$
106		1onn	$⊢ 1_{𝑜} \in ω$
107	106	a1i	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to 1_{𝑜} \in ω$
108		opelxpi	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to ⟨1^{st} (u), 1^{st} (v)⟩ \in (r \times s)$
109	107 108	opelxpd	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to ⟨1_{𝑜}, ⟨1^{st} (u), 1^{st} (v)⟩⟩ \in (ω \times (r \times s))$
110	105 109	eqeltrd	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (r \times s))$
111		xpeq12	$⊢ (a = r \land b = s) \to a \times b = r \times s$
112	111	xpeq2d	$⊢ (a = r \land b = s) \to ω \times (a \times b) = ω \times (r \times s)$
113	112	eleq2d	$⊢ (a = r \land b = s) \to (1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (a \times b)) \leftrightarrow 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (r \times s)))$
114	113	spc2egv	$⊢ (r \in V \land s \in V) \to (1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (r \times s)) \to \exists a \exists b 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (a \times b)))$
115	97 110 114	mpsyl	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to \exists a \exists b 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (a \times b))$
116		eleq1	$⊢ 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (1^{st} (t) \in (ω \times (a \times b)) \leftrightarrow 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (a \times b)))$
117	116	2exbidv	$⊢ 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (\exists a \exists b 1^{st} (t) \in (ω \times (a \times b)) \leftrightarrow \exists a \exists b 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \in (ω \times (a \times b)))$
118	115 117	syl5ibrcom	$⊢ (1^{st} (u) \in r \land 1^{st} (v) \in s) \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
119	118	ex	$⊢ 1^{st} (u) \in r \to (1^{st} (v) \in s \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
120	119	exlimdv	$⊢ 1^{st} (u) \in r \to (\exists s 1^{st} (v) \in s \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
121	120	com23	$⊢ 1^{st} (u) \in r \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (\exists s 1^{st} (v) \in s \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
122	121	exlimiv	$⊢ \exists r 1^{st} (u) \in r \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (\exists s 1^{st} (v) \in s \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
123	94 122	sylbi	$⊢ \exists s 1^{st} (u) \in s \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (\exists s 1^{st} (v) \in s \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
124	92 123	syl	$⊢ (u \in (\emptyset Sat \emptyset) (y) \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (\exists s 1^{st} (v) \in s \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
125	124	expcom	$⊢ \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to (u \in (\emptyset Sat \emptyset) (y) \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (\exists s 1^{st} (v) \in s \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
126	125	com24	$⊢ \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to (\exists s 1^{st} (v) \in s \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (u \in (\emptyset Sat \emptyset) (y) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
127	85 126	syld	$⊢ \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to (v \in (\emptyset Sat \emptyset) (y) \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (u \in (\emptyset Sat \emptyset) (y) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
128	127	adantl	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (v \in (\emptyset Sat \emptyset) (y) \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to (u \in (\emptyset Sat \emptyset) (y) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
129	128	com14	$⊢ u \in (\emptyset Sat \emptyset) (y) \to (v \in (\emptyset Sat \emptyset) (y) \to (1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
130	129	rexlimdv	$⊢ u \in (\emptyset Sat \emptyset) (y) \to (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
131	17 96	pm3.2i	$⊢ (ω \in V \land s \in V)$
132		df-goal	$⊢ [\forall_{𝑔} i 1^{st} (u)] = ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩$
133		2onn	$⊢ 2_{𝑜} \in ω$
134	133	a1i	$⊢ (1^{st} (u) \in s \land i \in ω) \to 2_{𝑜} \in ω$
135		opelxpi	$⊢ (i \in ω \land 1^{st} (u) \in s) \to ⟨i, 1^{st} (u)⟩ \in (ω \times s)$
136	135	ancoms	$⊢ (1^{st} (u) \in s \land i \in ω) \to ⟨i, 1^{st} (u)⟩ \in (ω \times s)$
137	134 136	opelxpd	$⊢ (1^{st} (u) \in s \land i \in ω) \to ⟨2_{𝑜}, ⟨i, 1^{st} (u)⟩⟩ \in (ω \times (ω \times s))$
138	132 137	eqeltrid	$⊢ (1^{st} (u) \in s \land i \in ω) \to [\forall_{𝑔} i 1^{st} (u)] \in (ω \times (ω \times s))$
139	138	3adant3	$⊢ (1^{st} (u) \in s \land i \in ω \land 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]) \to [\forall_{𝑔} i 1^{st} (u)] \in (ω \times (ω \times s))$
140		eleq1	$⊢ 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to (1^{st} (t) \in (ω \times (ω \times s)) \leftrightarrow [\forall_{𝑔} i 1^{st} (u)] \in (ω \times (ω \times s)))$
141	140	3ad2ant3	$⊢ (1^{st} (u) \in s \land i \in ω \land 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]) \to (1^{st} (t) \in (ω \times (ω \times s)) \leftrightarrow [\forall_{𝑔} i 1^{st} (u)] \in (ω \times (ω \times s)))$
142	139 141	mpbird	$⊢ (1^{st} (u) \in s \land i \in ω \land 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]) \to 1^{st} (t) \in (ω \times (ω \times s))$
143		xpeq12	$⊢ (a = ω \land b = s) \to a \times b = ω \times s$
144	143	xpeq2d	$⊢ (a = ω \land b = s) \to ω \times (a \times b) = ω \times (ω \times s)$
145	144	eleq2d	$⊢ (a = ω \land b = s) \to (1^{st} (t) \in (ω \times (a \times b)) \leftrightarrow 1^{st} (t) \in (ω \times (ω \times s)))$
146	145	spc2egv	$⊢ (ω \in V \land s \in V) \to (1^{st} (t) \in (ω \times (ω \times s)) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
147	131 142 146	mpsyl	$⊢ (1^{st} (u) \in s \land i \in ω \land 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))$
148	147	3exp	$⊢ 1^{st} (u) \in s \to (i \in ω \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
149	148	com23	$⊢ 1^{st} (u) \in s \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to (i \in ω \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
150	149	a1d	$⊢ 1^{st} (u) \in s \to (y \in ω \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to (i \in ω \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
151	150	exlimiv	$⊢ \exists s 1^{st} (u) \in s \to (y \in ω \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to (i \in ω \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
152	92 151	syl	$⊢ (u \in (\emptyset Sat \emptyset) (y) \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (y \in ω \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to (i \in ω \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
153	152	ex	$⊢ u \in (\emptyset Sat \emptyset) (y) \to (\forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to (y \in ω \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to (i \in ω \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))))$
154	153	impcomd	$⊢ u \in (\emptyset Sat \emptyset) (y) \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to (i \in ω \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
155	154	com24	$⊢ u \in (\emptyset Sat \emptyset) (y) \to (i \in ω \to (1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))))$
156	155	rexlimdv	$⊢ u \in (\emptyset Sat \emptyset) (y) \to (\exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)] \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
157	130 156	jaod	$⊢ u \in (\emptyset Sat \emptyset) (y) \to ((\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]) \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
158	157	rexlimiv	$⊢ \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]) \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
159	158	adantl	$⊢ (2^{nd} (t) = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)])) \to ((y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
160		eqeq1	$⊢ x = 1^{st} (t) \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
161	160	rexbidv	$⊢ x = 1^{st} (t) \to (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow \exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
162		eqeq1	$⊢ x = 1^{st} (t) \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)])$
163	162	rexbidv	$⊢ x = 1^{st} (t) \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)])$
164	161 163	orbi12d	$⊢ x = 1^{st} (t) \to ((\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]))$
165	164	rexbidv	$⊢ x = 1^{st} (t) \to (\exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]))$
166	165	anbi2d	$⊢ x = 1^{st} (t) \to ((z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)])))$
167		eqeq1	$⊢ z = 2^{nd} (t) \to (z = \emptyset \leftrightarrow 2^{nd} (t) = \emptyset)$
168	167	anbi1d	$⊢ z = 2^{nd} (t) \to ((z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (2^{nd} (t) = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)])))$
169	166 168	elopabi	$⊢ t \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \to (2^{nd} (t) = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) 1^{st} (t) = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω 1^{st} (t) = [\forall_{𝑔} i 1^{st} (u)]))$
170	159 169	syl11	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (t \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\} \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
171	77 170	jaod	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to ((t \in (\emptyset Sat \emptyset) (y) \lor t \in \{⟨x, z⟩ \| (z = \emptyset \land \exists u \in (\emptyset Sat \emptyset) (y) (\exists v \in (\emptyset Sat \emptyset) (y) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
172	72 171	sylbid	$⊢ (y \in ω \land \forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))) \to (t \in (\emptyset Sat \emptyset) (suc y) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
173	172	ex	$⊢ y \in ω \to (\forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to (t \in (\emptyset Sat \emptyset) (suc y) \to \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))))$
174	173	ralrimdv	$⊢ y \in ω \to (\forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to \forall t \in (\emptyset Sat \emptyset) (suc y) \exists a \exists b 1^{st} (t) \in (ω \times (a \times b)))$
175	75	cbvralvw	$⊢ \forall w \in (\emptyset Sat \emptyset) (suc y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \leftrightarrow \forall t \in (\emptyset Sat \emptyset) (suc y) \exists a \exists b 1^{st} (t) \in (ω \times (a \times b))$
176	174 175	imbitrrdi	$⊢ y \in ω \to (\forall w \in (\emptyset Sat \emptyset) (y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)) \to \forall w \in (\emptyset Sat \emptyset) (suc y) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b)))$
177	2 4 6 8 37 176	finds	$⊢ N \in ω \to \forall w \in (\emptyset Sat \emptyset) (N) \exists a \exists b 1^{st} (w) \in (ω \times (a \times b))$

Metamath Proof Explorer

Theorem sat1el2xp

Proof