satfrnmapom

Description: The range of the satisfaction predicate as function over wff codes in any model M and any binary relation E on M for a natural number N is a subset of the power set of all mappings from the natural numbers into the model M . (Contributed by AV, 13-Oct-2023)

		Ref	Expression
	Assertion	satfrnmapom	$⊢ (M \in V \land E \in W \land N \in ω) \to ran (M Sat E) (N) \subseteq 𝒫 (M^{ω})$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ a = \emptyset \to (M Sat E) (a) = (M Sat E) (\emptyset)$
2	1	rneqd	$⊢ a = \emptyset \to ran (M Sat E) (a) = ran (M Sat E) (\emptyset)$
3	2	eleq2d	$⊢ a = \emptyset \to (n \in ran (M Sat E) (a) \leftrightarrow n \in ran (M Sat E) (\emptyset))$
4	3	imbi1d	$⊢ a = \emptyset \to ((n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω})) \leftrightarrow (n \in ran (M Sat E) (\emptyset) \to n \in 𝒫 (M^{ω})))$
5	4	imbi2d	$⊢ a = \emptyset \to (((M \in V \land E \in W) \to (n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω}))) \leftrightarrow ((M \in V \land E \in W) \to (n \in ran (M Sat E) (\emptyset) \to n \in 𝒫 (M^{ω}))))$
6		fveq2	$⊢ a = b \to (M Sat E) (a) = (M Sat E) (b)$
7	6	rneqd	$⊢ a = b \to ran (M Sat E) (a) = ran (M Sat E) (b)$
8	7	eleq2d	$⊢ a = b \to (n \in ran (M Sat E) (a) \leftrightarrow n \in ran (M Sat E) (b))$
9	8	imbi1d	$⊢ a = b \to ((n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω})) \leftrightarrow (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))$
10	9	imbi2d	$⊢ a = b \to (((M \in V \land E \in W) \to (n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω}))) \leftrightarrow ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω}))))$
11		fveq2	$⊢ a = suc b \to (M Sat E) (a) = (M Sat E) (suc b)$
12	11	rneqd	$⊢ a = suc b \to ran (M Sat E) (a) = ran (M Sat E) (suc b)$
13	12	eleq2d	$⊢ a = suc b \to (n \in ran (M Sat E) (a) \leftrightarrow n \in ran (M Sat E) (suc b))$
14	13	imbi1d	$⊢ a = suc b \to ((n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω})) \leftrightarrow (n \in ran (M Sat E) (suc b) \to n \in 𝒫 (M^{ω})))$
15	14	imbi2d	$⊢ a = suc b \to (((M \in V \land E \in W) \to (n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω}))) \leftrightarrow ((M \in V \land E \in W) \to (n \in ran (M Sat E) (suc b) \to n \in 𝒫 (M^{ω}))))$
16		fveq2	$⊢ a = N \to (M Sat E) (a) = (M Sat E) (N)$
17	16	rneqd	$⊢ a = N \to ran (M Sat E) (a) = ran (M Sat E) (N)$
18	17	eleq2d	$⊢ a = N \to (n \in ran (M Sat E) (a) \leftrightarrow n \in ran (M Sat E) (N))$
19	18	imbi1d	$⊢ a = N \to ((n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω})) \leftrightarrow (n \in ran (M Sat E) (N) \to n \in 𝒫 (M^{ω})))$
20	19	imbi2d	$⊢ a = N \to (((M \in V \land E \in W) \to (n \in ran (M Sat E) (a) \to n \in 𝒫 (M^{ω}))) \leftrightarrow ((M \in V \land E \in W) \to (n \in ran (M Sat E) (N) \to n \in 𝒫 (M^{ω}))))$
21		eqid	$⊢ M Sat E = M Sat E$
22	21	satfv0	$⊢ (M \in V \land E \in W) \to (M Sat E) (\emptyset) = \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\}$
23	22	rneqd	$⊢ (M \in V \land E \in W) \to ran (M Sat E) (\emptyset) = ran \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\}$
24	23	eleq2d	$⊢ (M \in V \land E \in W) \to (n \in ran (M Sat E) (\emptyset) \leftrightarrow n \in ran \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\})$
25		rnopab	$⊢ ran \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\} = \{y \| \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\}$
26	25	eleq2i	$⊢ n \in ran \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\} \leftrightarrow n \in \{y \| \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\}$
27		vex	$⊢ n \in V$
28		eqeq1	$⊢ y = n \to (y = \{f \in (M^{ω}) \| f (i) E f (j)\} \leftrightarrow n = \{f \in (M^{ω}) \| f (i) E f (j)\})$
29	28	anbi2d	$⊢ y = n \to ((x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow (x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\}))$
30	29	2rexbidv	$⊢ y = n \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\}))$
31	30	exbidv	$⊢ y = n \to (\exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\}))$
32	27 31	elab	$⊢ n \in \{y \| \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\} \leftrightarrow \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\})$
33		ovex	$⊢ M^{ω} \in V$
34		ssrab2	$⊢ \{f \in (M^{ω}) \| f (i) E f (j)\} \subseteq M^{ω}$
35	33 34	elpwi2	$⊢ \{f \in (M^{ω}) \| f (i) E f (j)\} \in 𝒫 (M^{ω})$
36		eleq1	$⊢ n = \{f \in (M^{ω}) \| f (i) E f (j)\} \to (n \in 𝒫 (M^{ω}) \leftrightarrow \{f \in (M^{ω}) \| f (i) E f (j)\} \in 𝒫 (M^{ω}))$
37	35 36	mpbiri	$⊢ n = \{f \in (M^{ω}) \| f (i) E f (j)\} \to n \in 𝒫 (M^{ω})$
38	37	adantl	$⊢ (x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to n \in 𝒫 (M^{ω})$
39	38	a1i	$⊢ (i \in ω \land j \in ω) \to ((x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to n \in 𝒫 (M^{ω}))$
40	39	rexlimivv	$⊢ \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to n \in 𝒫 (M^{ω})$
41	40	exlimiv	$⊢ \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land n = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to n \in 𝒫 (M^{ω})$
42	32 41	sylbi	$⊢ n \in \{y \| \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\} \to n \in 𝒫 (M^{ω})$
43	42	a1i	$⊢ (M \in V \land E \in W) \to (n \in \{y \| \exists x \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\} \to n \in 𝒫 (M^{ω}))$
44	26 43	syl5bi	$⊢ (M \in V \land E \in W) \to (n \in ran \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\} \to n \in 𝒫 (M^{ω}))$
45	24 44	sylbid	$⊢ (M \in V \land E \in W) \to (n \in ran (M Sat E) (\emptyset) \to n \in 𝒫 (M^{ω}))$
46	21	satfvsuc	$⊢ (M \in V \land E \in W \land b \in ω) \to (M Sat E) (suc b) = (M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
47	46	3expa	$⊢ ((M \in V \land E \in W) \land b \in ω) \to (M Sat E) (suc b) = (M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
48	47	rneqd	$⊢ ((M \in V \land E \in W) \land b \in ω) \to ran (M Sat E) (suc b) = ran ((M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\})$
49		rnun	$⊢ ran ((M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) = ran (M Sat E) (b) \cup ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
50	48 49	eqtrdi	$⊢ ((M \in V \land E \in W) \land b \in ω) \to ran (M Sat E) (suc b) = ran (M Sat E) (b) \cup ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
51	50	eleq2d	$⊢ ((M \in V \land E \in W) \land b \in ω) \to (n \in ran (M Sat E) (suc b) \leftrightarrow n \in (ran (M Sat E) (b) \cup ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}))$
52		elun	$⊢ n \in (ran (M Sat E) (b) \cup ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (n \in ran (M Sat E) (b) \lor n \in ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\})$
53		rnopab	$⊢ ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} = \{y \| \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
54	53	eleq2i	$⊢ n \in ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \leftrightarrow n \in \{y \| \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
55		eqeq1	$⊢ y = n \to (y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \leftrightarrow n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
56	55	anbi2d	$⊢ y = n \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
57	56	rexbidv	$⊢ y = n \to (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
58		eqeq1	$⊢ y = n \to (y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \leftrightarrow n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
59	58	anbi2d	$⊢ y = n \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
60	59	rexbidv	$⊢ y = n \to (\exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
61	57 60	orbi12d	$⊢ y = n \to ((\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
62	61	rexbidv	$⊢ y = n \to (\exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
63	62	exbidv	$⊢ y = n \to (\exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \leftrightarrow \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
64	27 63	elab	$⊢ n \in \{y \| \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \leftrightarrow \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
65	54 64	bitri	$⊢ n \in ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\} \leftrightarrow \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
66	65	orbi2i	$⊢ (n \in ran (M Sat E) (b) \lor n \in ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (n \in ran (M Sat E) (b) \lor \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
67	52 66	bitri	$⊢ n \in (ran (M Sat E) (b) \cup ran \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}) \leftrightarrow (n \in ran (M Sat E) (b) \lor \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))$
68	51 67	syl6bb	$⊢ ((M \in V \land E \in W) \land b \in ω) \to (n \in ran (M Sat E) (suc b) \leftrightarrow (n \in ran (M Sat E) (b) \lor \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
69	68	expcom	$⊢ b \in ω \to ((M \in V \land E \in W) \to (n \in ran (M Sat E) (suc b) \leftrightarrow (n \in ran (M Sat E) (b) \lor \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))))$
70	69	adantr	$⊢ (b \in ω \land ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))) \to ((M \in V \land E \in W) \to (n \in ran (M Sat E) (suc b) \leftrightarrow (n \in ran (M Sat E) (b) \lor \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})))))$
71	70	imp	$⊢ ((b \in ω \land ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))) \land (M \in V \land E \in W)) \to (n \in ran (M Sat E) (suc b) \leftrightarrow (n \in ran (M Sat E) (b) \lor \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))))$
72		simpr	$⊢ (b \in ω \land ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))) \to ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))$
73	72	imp	$⊢ ((b \in ω \land ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))) \land (M \in V \land E \in W)) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω}))$
74		difss	$⊢ (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \subseteq M^{ω}$
75	33 74	elpwi2	$⊢ (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in 𝒫 (M^{ω})$
76		eleq1	$⊢ n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to (n \in 𝒫 (M^{ω}) \leftrightarrow (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \in 𝒫 (M^{ω}))$
77	75 76	mpbiri	$⊢ n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \to n \in 𝒫 (M^{ω})$
78	77	adantl	$⊢ (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to n \in 𝒫 (M^{ω})$
79	78	adantl	$⊢ (v \in (M Sat E) (b) \land (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))) \to n \in 𝒫 (M^{ω})$
80	79	rexlimiva	$⊢ \exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \to n \in 𝒫 (M^{ω})$
81		ssrab2	$⊢ \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \subseteq M^{ω}$
82	33 81	elpwi2	$⊢ \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in 𝒫 (M^{ω})$
83		eleq1	$⊢ n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to (n \in 𝒫 (M^{ω}) \leftrightarrow \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \in 𝒫 (M^{ω}))$
84	82 83	mpbiri	$⊢ n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \to n \in 𝒫 (M^{ω})$
85	84	adantl	$⊢ (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to n \in 𝒫 (M^{ω})$
86	85	a1i	$⊢ i \in ω \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to n \in 𝒫 (M^{ω}))$
87	86	rexlimiv	$⊢ \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \to n \in 𝒫 (M^{ω})$
88	80 87	jaoi	$⊢ (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to n \in 𝒫 (M^{ω})$
89	88	a1i	$⊢ u \in (M Sat E) (b) \to ((\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to n \in 𝒫 (M^{ω}))$
90	89	rexlimiv	$⊢ \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to n \in 𝒫 (M^{ω})$
91	90	exlimiv	$⊢ \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to n \in 𝒫 (M^{ω})$
92	91	a1i	$⊢ ((b \in ω \land ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))) \land (M \in V \land E \in W)) \to (\exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})) \to n \in 𝒫 (M^{ω}))$
93	73 92	jaod	$⊢ ((b \in ω \land ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))) \land (M \in V \land E \in W)) \to ((n \in ran (M Sat E) (b) \lor \exists x \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land n = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land n = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))) \to n \in 𝒫 (M^{ω}))$
94	71 93	sylbid	$⊢ ((b \in ω \land ((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω})))) \land (M \in V \land E \in W)) \to (n \in ran (M Sat E) (suc b) \to n \in 𝒫 (M^{ω}))$
95	94	exp31	$⊢ b \in ω \to (((M \in V \land E \in W) \to (n \in ran (M Sat E) (b) \to n \in 𝒫 (M^{ω}))) \to ((M \in V \land E \in W) \to (n \in ran (M Sat E) (suc b) \to n \in 𝒫 (M^{ω}))))$
96	5 10 15 20 45 95	finds	$⊢ N \in ω \to ((M \in V \land E \in W) \to (n \in ran (M Sat E) (N) \to n \in 𝒫 (M^{ω})))$
97	96	com12	$⊢ (M \in V \land E \in W) \to (N \in ω \to (n \in ran (M Sat E) (N) \to n \in 𝒫 (M^{ω})))$
98	97	3impia	$⊢ (M \in V \land E \in W \land N \in ω) \to (n \in ran (M Sat E) (N) \to n \in 𝒫 (M^{ω}))$
99	98	ssrdv	$⊢ (M \in V \land E \in W \land N \in ω) \to ran (M Sat E) (N) \subseteq 𝒫 (M^{ω})$

Metamath Proof Explorer

Theorem satfrnmapom

Proof