satf0op

Description: An element of a value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation expressed as ordered pair. (Contributed by AV, 19-Sep-2023)

		Ref	Expression
	Hypothesis	satf0op.s	$⊢ S = \emptyset Sat \emptyset$
	Assertion	satf0op	$⊢ N \in ω \to (X \in S (N) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (N)))$

Proof

Step	Hyp	Ref	Expression
1		satf0op.s	$⊢ S = \emptyset Sat \emptyset$
2		fveq2	$⊢ y = \emptyset \to S (y) = S (\emptyset)$
3	2	eleq2d	$⊢ y = \emptyset \to (X \in S (y) \leftrightarrow X \in S (\emptyset))$
4	2	eleq2d	$⊢ y = \emptyset \to (⟨x, \emptyset⟩ \in S (y) \leftrightarrow ⟨x, \emptyset⟩ \in S (\emptyset))$
5	4	anbi2d	$⊢ y = \emptyset \to ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset)))$
6	5	exbidv	$⊢ y = \emptyset \to (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset)))$
7	3 6	bibi12d	$⊢ y = \emptyset \to ((X \in S (y) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y))) \leftrightarrow (X \in S (\emptyset) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset))))$
8		fveq2	$⊢ y = z \to S (y) = S (z)$
9	8	eleq2d	$⊢ y = z \to (X \in S (y) \leftrightarrow X \in S (z))$
10	8	eleq2d	$⊢ y = z \to (⟨x, \emptyset⟩ \in S (y) \leftrightarrow ⟨x, \emptyset⟩ \in S (z))$
11	10	anbi2d	$⊢ y = z \to ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))$
12	11	exbidv	$⊢ y = z \to (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))$
13	9 12	bibi12d	$⊢ y = z \to ((X \in S (y) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y))) \leftrightarrow (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z))))$
14		fveq2	$⊢ y = suc z \to S (y) = S (suc z)$
15	14	eleq2d	$⊢ y = suc z \to (X \in S (y) \leftrightarrow X \in S (suc z))$
16	14	eleq2d	$⊢ y = suc z \to (⟨x, \emptyset⟩ \in S (y) \leftrightarrow ⟨x, \emptyset⟩ \in S (suc z))$
17	16	anbi2d	$⊢ y = suc z \to ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z)))$
18	17	exbidv	$⊢ y = suc z \to (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z)))$
19	15 18	bibi12d	$⊢ y = suc z \to ((X \in S (y) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y))) \leftrightarrow (X \in S (suc z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z))))$
20		fveq2	$⊢ y = N \to S (y) = S (N)$
21	20	eleq2d	$⊢ y = N \to (X \in S (y) \leftrightarrow X \in S (N))$
22	20	eleq2d	$⊢ y = N \to (⟨x, \emptyset⟩ \in S (y) \leftrightarrow ⟨x, \emptyset⟩ \in S (N))$
23	22	anbi2d	$⊢ y = N \to ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (N)))$
24	23	exbidv	$⊢ y = N \to (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y)) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (N)))$
25	21 24	bibi12d	$⊢ y = N \to ((X \in S (y) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (y))) \leftrightarrow (X \in S (N) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (N))))$
26	1	fveq1i	$⊢ S (\emptyset) = (\emptyset Sat \emptyset) (\emptyset)$
27		satf00	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
28	26 27	eqtri	$⊢ S (\emptyset) = \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
29	28	eleq2i	$⊢ X \in S (\emptyset) \leftrightarrow X \in \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}$
30		elopab	$⊢ X \in \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\} \leftrightarrow \exists x \exists y (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j))$
31		opeq2	$⊢ y = \emptyset \to ⟨x, y⟩ = ⟨x, \emptyset⟩$
32	31	adantr	$⊢ (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \to ⟨x, y⟩ = ⟨x, \emptyset⟩$
33	32	eqeq2d	$⊢ (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨x, \emptyset⟩)$
34	33	biimpd	$⊢ (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \to (X = ⟨x, y⟩ \to X = ⟨x, \emptyset⟩)$
35	34	impcom	$⊢ (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to X = ⟨x, \emptyset⟩$
36		eqidd	$⊢ y = \emptyset \to \emptyset = \emptyset$
37	36	anim1i	$⊢ (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \to (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)$
38	37	adantl	$⊢ (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)$
39		satf00	$⊢ (\emptyset Sat \emptyset) (\emptyset) = \{⟨y, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω y = i \in_{𝑔} j)\}$
40	26 39	eqtri	$⊢ S (\emptyset) = \{⟨y, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω y = i \in_{𝑔} j)\}$
41	40	eleq2i	$⊢ ⟨x, \emptyset⟩ \in S (\emptyset) \leftrightarrow ⟨x, \emptyset⟩ \in \{⟨y, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω y = i \in_{𝑔} j)\}$
42		vex	$⊢ x \in V$
43		0ex	$⊢ \emptyset \in V$
44		eqeq1	$⊢ z = \emptyset \to (z = \emptyset \leftrightarrow \emptyset = \emptyset)$
45		eqeq1	$⊢ y = x \to (y = i \in_{𝑔} j \leftrightarrow x = i \in_{𝑔} j)$
46	45	2rexbidv	$⊢ y = x \to (\exists i \in ω \exists j \in ω y = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)$
47	44 46	bi2anan9r	$⊢ (y = x \land z = \emptyset) \to ((z = \emptyset \land \exists i \in ω \exists j \in ω y = i \in_{𝑔} j) \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j))$
48	42 43 47	opelopaba	$⊢ ⟨x, \emptyset⟩ \in \{⟨y, z⟩ \| (z = \emptyset \land \exists i \in ω \exists j \in ω y = i \in_{𝑔} j)\} \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)$
49	41 48	bitri	$⊢ ⟨x, \emptyset⟩ \in S (\emptyset) \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)$
50	38 49	sylibr	$⊢ (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to ⟨x, \emptyset⟩ \in S (\emptyset)$
51	35 50	jca	$⊢ (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset))$
52	51	exlimiv	$⊢ \exists y (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset))$
53	31	eqeq2d	$⊢ y = \emptyset \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨x, \emptyset⟩)$
54		eqeq1	$⊢ y = \emptyset \to (y = \emptyset \leftrightarrow \emptyset = \emptyset)$
55	54	anbi1d	$⊢ y = \emptyset \to ((y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j) \leftrightarrow (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j))$
56	53 55	anbi12d	$⊢ y = \emptyset \to ((X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \leftrightarrow (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)))$
57	43 56	spcev	$⊢ (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \to \exists y (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j))$
58	49 57	sylan2b	$⊢ (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset)) \to \exists y (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j))$
59	52 58	impbii	$⊢ \exists y (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \leftrightarrow (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset))$
60	59	exbii	$⊢ \exists x \exists y (X = ⟨x, y⟩ \land (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset))$
61	29 30 60	3bitri	$⊢ X \in S (\emptyset) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (\emptyset))$
62	1	satf0suc	$⊢ z \in ω \to S (suc z) = S (z) \cup \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}$
63	62	eleq2d	$⊢ z \in ω \to (X \in S (suc z) \leftrightarrow X \in (S (z) \cup \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}))$
64		elun	$⊢ X \in (S (z) \cup \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (X \in S (z) \lor X \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\})$
65	64	a1i	$⊢ z \in ω \to (X \in (S (z) \cup \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (X \in S (z) \lor X \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}))$
66		elopab	$⊢ X \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\} \leftrightarrow \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
67	66	a1i	$⊢ z \in ω \to (X \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\} \leftrightarrow \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))))$
68	67	orbi2d	$⊢ z \in ω \to ((X \in S (z) \lor X \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (X \in S (z) \lor \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))))$
69	63 65 68	3bitrd	$⊢ z \in ω \to (X \in S (suc z) \leftrightarrow (X \in S (z) \lor \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))))$
70	69	adantr	$⊢ (z \in ω \land (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))) \to (X \in S (suc z) \leftrightarrow (X \in S (z) \lor \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))))$
71		simpr	$⊢ (z \in ω \land (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))) \to (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))$
72		opeq2	$⊢ b = \emptyset \to ⟨a, b⟩ = ⟨a, \emptyset⟩$
73	72	eqeq2d	$⊢ b = \emptyset \to (X = ⟨a, b⟩ \leftrightarrow X = ⟨a, \emptyset⟩)$
74	73	biimpd	$⊢ b = \emptyset \to (X = ⟨a, b⟩ \to X = ⟨a, \emptyset⟩)$
75	74	adantr	$⊢ (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])) \to (X = ⟨a, b⟩ \to X = ⟨a, \emptyset⟩)$
76	75	impcom	$⊢ (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \to X = ⟨a, \emptyset⟩$
77		eqidd	$⊢ (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \to \emptyset = \emptyset$
78		simpr	$⊢ (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])) \to \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])$
79	78	adantl	$⊢ (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \to \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])$
80	77 79	jca	$⊢ (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \to (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))$
81	76 80	jca	$⊢ (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \to (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
82	81	exlimiv	$⊢ \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \to (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
83		eqeq1	$⊢ b = \emptyset \to (b = \emptyset \leftrightarrow \emptyset = \emptyset)$
84	83	anbi1d	$⊢ b = \emptyset \to ((b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
85	73 84	anbi12d	$⊢ b = \emptyset \to ((X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))))$
86	43 85	spcev	$⊢ (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \to \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
87	82 86	impbii	$⊢ \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
88	87	exbii	$⊢ \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow \exists a (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
89	88	a1i	$⊢ z \in ω \to (\exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow \exists a (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))))$
90		opeq1	$⊢ x = a \to ⟨x, \emptyset⟩ = ⟨a, \emptyset⟩$
91	90	eqeq2d	$⊢ x = a \to (X = ⟨x, \emptyset⟩ \leftrightarrow X = ⟨a, \emptyset⟩)$
92		eqeq1	$⊢ x = a \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
93	92	rexbidv	$⊢ x = a \to (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow \exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
94		eqeq1	$⊢ x = a \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow a = [\forall_{𝑔} i 1^{st} (u)])$
95	94	rexbidv	$⊢ x = a \to (\exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])$
96	93 95	orbi12d	$⊢ x = a \to ((\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))$
97	96	rexbidv	$⊢ x = a \to (\exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))$
98	97	anbi2d	$⊢ x = a \to ((\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
99	91 98	anbi12d	$⊢ x = a \to ((X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))))$
100	99	cbvexvw	$⊢ \exists x (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow \exists a (X = ⟨a, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))$
101	89 100	syl6bbr	$⊢ z \in ω \to (\exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
102	101	adantr	$⊢ (z \in ω \land (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))) \to (\exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
103	71 102	orbi12d	$⊢ (z \in ω \land (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))) \to ((X \in S (z) \lor \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)) \lor \exists x (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))))$
104		19.43	$⊢ \exists x ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)) \lor (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)) \lor \exists x (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
105		andi	$⊢ (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)) \lor (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
106	105	bicomi	$⊢ ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)) \lor (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
107	106	exbii	$⊢ \exists x ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)) \lor (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
108	104 107	bitr3i	$⊢ (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)) \lor \exists x (X = ⟨x, \emptyset⟩ \land (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
109	103 108	syl6bb	$⊢ (z \in ω \land (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))) \to ((X \in S (z) \lor \exists a \exists b (X = ⟨a, b⟩ \land (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))))$
110	62	eleq2d	$⊢ z \in ω \to (⟨x, \emptyset⟩ \in S (suc z) \leftrightarrow ⟨x, \emptyset⟩ \in (S (z) \cup \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}))$
111		elun	$⊢ ⟨x, \emptyset⟩ \in (S (z) \cup \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (⟨x, \emptyset⟩ \in S (z) \lor ⟨x, \emptyset⟩ \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\})$
112		eqeq1	$⊢ a = x \to (a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
113	112	rexbidv	$⊢ a = x \to (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow \exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
114		eqeq1	$⊢ a = x \to (a = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow x = [\forall_{𝑔} i 1^{st} (u)])$
115	114	rexbidv	$⊢ a = x \to (\exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])$
116	113 115	orbi12d	$⊢ a = x \to ((\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
117	116	rexbidv	$⊢ a = x \to (\exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]) \leftrightarrow \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
118	83 117	bi2anan9r	$⊢ (a = x \land b = \emptyset) \to ((b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)])) \leftrightarrow (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
119	42 43 118	opelopaba	$⊢ ⟨x, \emptyset⟩ \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\} \leftrightarrow (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))$
120	119	orbi2i	$⊢ (⟨x, \emptyset⟩ \in S (z) \lor ⟨x, \emptyset⟩ \in \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
121	111 120	bitri	$⊢ ⟨x, \emptyset⟩ \in (S (z) \cup \{⟨a, b⟩ \| (b = \emptyset \land \exists u \in S (z) (\exists v \in S (z) a = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω a = [\forall_{𝑔} i 1^{st} (u)]))\}) \leftrightarrow (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))$
122	110 121	syl6bb	$⊢ z \in ω \to (⟨x, \emptyset⟩ \in S (suc z) \leftrightarrow (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))))$
123	122	anbi2d	$⊢ z \in ω \to ((X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z)) \leftrightarrow (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))))$
124	123	exbidv	$⊢ z \in ω \to (\exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z)) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))))$
125	124	bicomd	$⊢ z \in ω \to (\exists x (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z)))$
126	125	adantr	$⊢ (z \in ω \land (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))) \to (\exists x (X = ⟨x, \emptyset⟩ \land (⟨x, \emptyset⟩ \in S (z) \lor (\emptyset = \emptyset \land \exists u \in S (z) (\exists v \in S (z) x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)])))) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z)))$
127	70 109 126	3bitrd	$⊢ (z \in ω \land (X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z)))) \to (X \in S (suc z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z)))$
128	127	ex	$⊢ z \in ω \to ((X \in S (z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (z))) \to (X \in S (suc z) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (suc z))))$
129	7 13 19 25 61 128	finds	$⊢ N \in ω \to (X \in S (N) \leftrightarrow \exists x (X = ⟨x, \emptyset⟩ \land ⟨x, \emptyset⟩ \in S (N)))$

Metamath Proof Explorer

Theorem satf0op

Proof