satfbrsuc

Description: The binary relation of a satisfaction predicate as function over wff codes at a successor. (Contributed by AV, 13-Oct-2023)

	Ref	Expression
Hypotheses	satfbrsuc.s	$⊢ S = M Sat E$
	satfbrsuc.p	$⊢ P = S (N)$
Assertion	satfbrsuc	$⊢ ((M \in V \land E \in W) \land N \in ω \land (A \in X \land B \in Y)) \to (A S (suc N) B \leftrightarrow (A P B \lor \exists u \in P (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$

Proof

Step	Hyp	Ref	Expression
1		satfbrsuc.s	$⊢ S = M Sat E$
2		satfbrsuc.p	$⊢ P = S (N)$
3	1	satfvsuc	$⊢ (M \in V \land E \in W \land N \in ω) \to S (suc N) = S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
4	3	3expa	$⊢ ((M \in V \land E \in W) \land N \in ω) \to S (suc N) = S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
5	4	3adant3	$⊢ ((M \in V \land E \in W) \land N \in ω \land (A \in X \land B \in Y)) \to S (suc N) = S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
6	5	breqd	$⊢ ((M \in V \land E \in W) \land N \in ω \land (A \in X \land B \in Y)) \to (A S (suc N) B \leftrightarrow A (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) B)$
7		brun	$⊢ A (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) B \leftrightarrow (A S (N) B \lor A \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} B)$
8	2	eqcomi	$⊢ S (N) = P$
9	8	breqi	$⊢ A S (N) B \leftrightarrow A P B$
10	9	a1i	$⊢ (A \in X \land B \in Y) \to (A S (N) B \leftrightarrow A P B)$
11		eqeq1	$⊢ x = A \to (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \leftrightarrow A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
12		eqeq1	$⊢ y = B \to (y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \leftrightarrow B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
13	11 12	bi2anan9	$⊢ (x = A \land y = B) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
14	13	rexbidv	$⊢ (x = A \land y = B) \to (\exists v \in P (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
15		eqeq1	$⊢ x = A \to (x = [\forall_{𝑔} i 1^{st} (u)] \leftrightarrow A = [\forall_{𝑔} i 1^{st} (u)])$
16		eqeq1	$⊢ y = B \to (y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \leftrightarrow B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
17	15 16	bi2anan9	$⊢ (x = A \land y = B) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
18	17	rexbidv	$⊢ (x = A \land y = B) \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
19	14 18	orbi12d	$⊢ (x = A \land y = B) \to ((\exists v \in P (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
20	19	rexbidv	$⊢ (x = A \land y = B) \to (\exists u \in P (\exists v \in P (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in P (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
21	8	rexeqi	$⊢ \exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in P (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
22	21	orbi1i	$⊢ (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists v \in P (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
23	8 22	rexeqbii	$⊢ \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in P (\exists v \in P (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
24	23	opabbii	$⊢ \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \{⟨x, y⟩ \| \exists u \in P (\exists v \in P (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
25	20 24	brabga	$⊢ (A \in X \land B \in Y) \to (A \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} B \leftrightarrow \exists u \in P (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
26	10 25	orbi12d	$⊢ (A \in X \land B \in Y) \to ((A S (N) B \lor A \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} B) \leftrightarrow (A P B \lor \exists u \in P (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
27	7 26	bitrid	$⊢ (A \in X \land B \in Y) \to (A (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) B \leftrightarrow (A P B \lor \exists u \in P (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
28	27	3ad2ant3	$⊢ ((M \in V \land E \in W) \land N \in ω \land (A \in X \land B \in Y)) \to (A (S (N) \cup \{⟨x, y⟩ \| \exists u \in S (N) (\exists v \in S (N) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) B \leftrightarrow (A P B \lor \exists u \in P (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
29	6 28	bitrd	$⊢ ((M \in V \land E \in W) \land N \in ω \land (A \in X \land B \in Y)) \to (A S (suc N) B \leftrightarrow (A P B \lor \exists u \in P (\exists v \in P (A = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land B = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (A = [\forall_{𝑔} i 1^{st} (u)] \land B = \{f \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({f ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$

Metamath Proof Explorer

Theorem satfbrsuc

Proof