satefvfmla1

Description: The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023)

		Ref	Expression
	Hypothesis	satfv1fvfmla1.x	$⊢ X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
	Assertion	satefvfmla1	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to M {Sat}_{\in} X = \{a \in (M^{ω}) \| (\neg a (I) \in a (J) \lor \neg a (K) \in a (L))\}$

Proof

Step	Hyp	Ref	Expression
1		satfv1fvfmla1.x	$⊢ X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
2	1	ovexi	$⊢ X \in V$
3	2	jctr	$⊢ M \in V \to (M \in V \land X \in V)$
4	3	3ad2ant1	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M \in V \land X \in V)$
5		satefv	$⊢ (M \in V \land X \in V) \to M {Sat}_{\in} X = (M Sat (E \cap (M \times M))) (ω) (X)$
6	4 5	syl	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to M {Sat}_{\in} X = (M Sat (E \cap (M \times M))) (ω) (X)$
7		sqxpexg	$⊢ M \in V \to M \times M \in V$
8		inex2g	$⊢ M \times M \in V \to E \cap (M \times M) \in V$
9	7 8	syl	$⊢ M \in V \to E \cap (M \times M) \in V$
10	9	ancli	$⊢ M \in V \to (M \in V \land E \cap (M \times M) \in V)$
11	10	3ad2ant1	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M \in V \land E \cap (M \times M) \in V)$
12		satom	$⊢ (M \in V \land E \cap (M \times M) \in V) \to (M Sat (E \cap (M \times M))) (ω) = ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i)$
13	11 12	syl	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat (E \cap (M \times M))) (ω) = ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i)$
14	13	fveq1d	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat (E \cap (M \times M))) (ω) (X) = ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i) (X)$
15		satfun	$⊢ (M \in V \land E \cap (M \times M) \in V) \to (M Sat (E \cap (M \times M))) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω})$
16	11 15	syl	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat (E \cap (M \times M))) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω})$
17	16	ffund	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to Fun (M Sat (E \cap (M \times M))) (ω)$
18	13	eqcomd	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i) = (M Sat (E \cap (M \times M))) (ω)$
19	18	funeqd	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (Fun ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i) \leftrightarrow Fun (M Sat (E \cap (M \times M))) (ω))$
20	17 19	mpbird	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to Fun ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i)$
21		1onn	$⊢ 1_{𝑜} \in ω$
22	21	a1i	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to 1_{𝑜} \in ω$
23	1	2goelgoanfmla1	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in Fmla (1_{𝑜})$
24	23	3adant1	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in Fmla (1_{𝑜})$
25	21	a1i	$⊢ M \in V \to 1_{𝑜} \in ω$
26		satfdmfmla	$⊢ (M \in V \land E \cap (M \times M) \in V \land 1_{𝑜} \in ω) \to dom (M Sat (E \cap (M \times M))) (1_{𝑜}) = Fmla (1_{𝑜})$
27	9 25 26	mpd3an23	$⊢ M \in V \to dom (M Sat (E \cap (M \times M))) (1_{𝑜}) = Fmla (1_{𝑜})$
28	27	3ad2ant1	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to dom (M Sat (E \cap (M \times M))) (1_{𝑜}) = Fmla (1_{𝑜})$
29	24 28	eleqtrrd	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in dom (M Sat (E \cap (M \times M))) (1_{𝑜})$
30		eqid	$⊢ ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i) = ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i)$
31	30	fviunfun	$⊢ (Fun ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i) \land 1_{𝑜} \in ω \land X \in dom (M Sat (E \cap (M \times M))) (1_{𝑜})) \to ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i) (X) = (M Sat (E \cap (M \times M))) (1_{𝑜}) (X)$
32	20 22 29 31	syl3anc	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to ⋃_{i \in ω} (M Sat (E \cap (M \times M))) (i) (X) = (M Sat (E \cap (M \times M))) (1_{𝑜}) (X)$
33	14 32	eqtrd	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat (E \cap (M \times M))) (ω) (X) = (M Sat (E \cap (M \times M))) (1_{𝑜}) (X)$
34	1	satfv1fvfmla1	$⊢ ((M \in V \land E \cap (M \times M) \in V) \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat (E \cap (M \times M))) (1_{𝑜}) (X) = \{a \in (M^{ω}) \| (\neg a (I) (E \cap (M \times M)) a (J) \lor \neg a (K) (E \cap (M \times M)) a (L))\}$
35	10 34	syl3an1	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat (E \cap (M \times M))) (1_{𝑜}) (X) = \{a \in (M^{ω}) \| (\neg a (I) (E \cap (M \times M)) a (J) \lor \neg a (K) (E \cap (M \times M)) a (L))\}$
36		brin	$⊢ a (I) (E \cap (M \times M)) a (J) \leftrightarrow (a (I) E a (J) \land a (I) (M \times M) a (J))$
37		elmapi	$⊢ a \in (M^{ω}) \to a : ω ⟶ M$
38		ffvelrn	$⊢ (a : ω ⟶ M \land I \in ω) \to a (I) \in M$
39	38	ex	$⊢ a : ω ⟶ M \to (I \in ω \to a (I) \in M)$
40	37 39	syl	$⊢ a \in (M^{ω}) \to (I \in ω \to a (I) \in M)$
41		ffvelrn	$⊢ (a : ω ⟶ M \land J \in ω) \to a (J) \in M$
42	41	ex	$⊢ a : ω ⟶ M \to (J \in ω \to a (J) \in M)$
43	37 42	syl	$⊢ a \in (M^{ω}) \to (J \in ω \to a (J) \in M)$
44	40 43	anim12d	$⊢ a \in (M^{ω}) \to ((I \in ω \land J \in ω) \to (a (I) \in M \land a (J) \in M))$
45	44	com12	$⊢ (I \in ω \land J \in ω) \to (a \in (M^{ω}) \to (a (I) \in M \land a (J) \in M))$
46	45	3ad2ant2	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (a \in (M^{ω}) \to (a (I) \in M \land a (J) \in M))$
47	46	imp	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (a (I) \in M \land a (J) \in M)$
48		brxp	$⊢ a (I) (M \times M) a (J) \leftrightarrow (a (I) \in M \land a (J) \in M)$
49	47 48	sylibr	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to a (I) (M \times M) a (J)$
50	49	biantrud	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (a (I) E a (J) \leftrightarrow (a (I) E a (J) \land a (I) (M \times M) a (J)))$
51		fvex	$⊢ a (J) \in V$
52	51	epeli	$⊢ a (I) E a (J) \leftrightarrow a (I) \in a (J)$
53	50 52	bitr3di	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to ((a (I) E a (J) \land a (I) (M \times M) a (J)) \leftrightarrow a (I) \in a (J))$
54	36 53	syl5bb	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (a (I) (E \cap (M \times M)) a (J) \leftrightarrow a (I) \in a (J))$
55	54	notbid	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (\neg a (I) (E \cap (M \times M)) a (J) \leftrightarrow \neg a (I) \in a (J))$
56		brin	$⊢ a (K) (E \cap (M \times M)) a (L) \leftrightarrow (a (K) E a (L) \land a (K) (M \times M) a (L))$
57		ffvelrn	$⊢ (a : ω ⟶ M \land K \in ω) \to a (K) \in M$
58	57	ex	$⊢ a : ω ⟶ M \to (K \in ω \to a (K) \in M)$
59	37 58	syl	$⊢ a \in (M^{ω}) \to (K \in ω \to a (K) \in M)$
60		ffvelrn	$⊢ (a : ω ⟶ M \land L \in ω) \to a (L) \in M$
61	60	ex	$⊢ a : ω ⟶ M \to (L \in ω \to a (L) \in M)$
62	37 61	syl	$⊢ a \in (M^{ω}) \to (L \in ω \to a (L) \in M)$
63	59 62	anim12d	$⊢ a \in (M^{ω}) \to ((K \in ω \land L \in ω) \to (a (K) \in M \land a (L) \in M))$
64	63	com12	$⊢ (K \in ω \land L \in ω) \to (a \in (M^{ω}) \to (a (K) \in M \land a (L) \in M))$
65	64	3ad2ant3	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (a \in (M^{ω}) \to (a (K) \in M \land a (L) \in M))$
66	65	imp	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (a (K) \in M \land a (L) \in M)$
67		brxp	$⊢ a (K) (M \times M) a (L) \leftrightarrow (a (K) \in M \land a (L) \in M)$
68	66 67	sylibr	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to a (K) (M \times M) a (L)$
69	68	biantrud	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (a (K) E a (L) \leftrightarrow (a (K) E a (L) \land a (K) (M \times M) a (L)))$
70		fvex	$⊢ a (L) \in V$
71	70	epeli	$⊢ a (K) E a (L) \leftrightarrow a (K) \in a (L)$
72	69 71	bitr3di	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to ((a (K) E a (L) \land a (K) (M \times M) a (L)) \leftrightarrow a (K) \in a (L))$
73	56 72	syl5bb	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (a (K) (E \cap (M \times M)) a (L) \leftrightarrow a (K) \in a (L))$
74	73	notbid	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to (\neg a (K) (E \cap (M \times M)) a (L) \leftrightarrow \neg a (K) \in a (L))$
75	55 74	orbi12d	$⊢ ((M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land a \in (M^{ω})) \to ((\neg a (I) (E \cap (M \times M)) a (J) \lor \neg a (K) (E \cap (M \times M)) a (L)) \leftrightarrow (\neg a (I) \in a (J) \lor \neg a (K) \in a (L)))$
76	75	rabbidva	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to \{a \in (M^{ω}) \| (\neg a (I) (E \cap (M \times M)) a (J) \lor \neg a (K) (E \cap (M \times M)) a (L))\} = \{a \in (M^{ω}) \| (\neg a (I) \in a (J) \lor \neg a (K) \in a (L))\}$
77	35 76	eqtrd	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (M Sat (E \cap (M \times M))) (1_{𝑜}) (X) = \{a \in (M^{ω}) \| (\neg a (I) \in a (J) \lor \neg a (K) \in a (L))\}$
78	6 33 77	3eqtrd	$⊢ (M \in V \land (I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to M {Sat}_{\in} X = \{a \in (M^{ω}) \| (\neg a (I) \in a (J) \lor \neg a (K) \in a (L))\}$

Metamath Proof Explorer

Theorem satefvfmla1

Proof