2goelgoanfmla1

Description: Two Godel-sets of membership combined with a Godel-set for NAND is a Godel formula of height 1. (Contributed by AV, 17-Nov-2023)

		Ref	Expression
	Hypothesis	satfv1fvfmla1.x	$⊢ X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
	Assertion	2goelgoanfmla1	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in Fmla (1_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		satfv1fvfmla1.x	$⊢ X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
2		simpll	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to I \in ω$
3		simplr	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to J \in ω$
4		simprl	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to K \in ω$
5		simprr	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to L \in ω$
6		oveq2	$⊢ n = L \to K \in_{𝑔} n = K \in_{𝑔} L$
7	6	oveq2d	$⊢ n = L \to (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n) = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
8	7	eqeq2d	$⊢ n = L \to (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n) \leftrightarrow X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L))$
9	8	adantl	$⊢ (((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \land n = L) \to (X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n) \leftrightarrow X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L))$
10	1	a1i	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} L)$
11	5 9 10	rspcedvd	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to \exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n)$
12	11	orcd	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (\exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n) \lor X = [\forall_{𝑔} K (I \in_{𝑔} J)])$
13		oveq1	$⊢ i = I \to i \in_{𝑔} j = I \in_{𝑔} j$
14	13	oveq1d	$⊢ i = I \to (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n)$
15	14	eqeq2d	$⊢ i = I \to (X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n))$
16	15	rexbidv	$⊢ i = I \to (\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow \exists n \in ω X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n))$
17		eqidd	$⊢ i = I \to k = k$
18	17 13	goaleq12d	$⊢ i = I \to [\forall_{𝑔} k (i \in_{𝑔} j)] = [\forall_{𝑔} k (I \in_{𝑔} j)]$
19	18	eqeq2d	$⊢ i = I \to (X = [\forall_{𝑔} k (i \in_{𝑔} j)] \leftrightarrow X = [\forall_{𝑔} k (I \in_{𝑔} j)])$
20	16 19	orbi12d	$⊢ i = I \to ((\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow (\exists n \in ω X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (I \in_{𝑔} j)]))$
21		oveq2	$⊢ j = J \to I \in_{𝑔} j = I \in_{𝑔} J$
22	21	oveq1d	$⊢ j = J \to (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n)$
23	22	eqeq2d	$⊢ j = J \to (X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n))$
24	23	rexbidv	$⊢ j = J \to (\exists n \in ω X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow \exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n))$
25		eqidd	$⊢ j = J \to k = k$
26	25 21	goaleq12d	$⊢ j = J \to [\forall_{𝑔} k (I \in_{𝑔} j)] = [\forall_{𝑔} k (I \in_{𝑔} J)]$
27	26	eqeq2d	$⊢ j = J \to (X = [\forall_{𝑔} k (I \in_{𝑔} j)] \leftrightarrow X = [\forall_{𝑔} k (I \in_{𝑔} J)])$
28	24 27	orbi12d	$⊢ j = J \to ((\exists n \in ω X = (I \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (I \in_{𝑔} j)]) \leftrightarrow (\exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (I \in_{𝑔} J)]))$
29		oveq1	$⊢ k = K \to k \in_{𝑔} n = K \in_{𝑔} n$
30	29	oveq2d	$⊢ k = K \to (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n) = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n)$
31	30	eqeq2d	$⊢ k = K \to (X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n))$
32	31	rexbidv	$⊢ k = K \to (\exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow \exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n))$
33		id	$⊢ k = K \to k = K$
34		eqidd	$⊢ k = K \to I \in_{𝑔} J = I \in_{𝑔} J$
35	33 34	goaleq12d	$⊢ k = K \to [\forall_{𝑔} k (I \in_{𝑔} J)] = [\forall_{𝑔} K (I \in_{𝑔} J)]$
36	35	eqeq2d	$⊢ k = K \to (X = [\forall_{𝑔} k (I \in_{𝑔} J)] \leftrightarrow X = [\forall_{𝑔} K (I \in_{𝑔} J)])$
37	32 36	orbi12d	$⊢ k = K \to ((\exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (I \in_{𝑔} J)]) \leftrightarrow (\exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n) \lor X = [\forall_{𝑔} K (I \in_{𝑔} J)]))$
38	20 28 37	rspc3ev	$⊢ ((I \in ω \land J \in ω \land K \in ω) \land (\exists n \in ω X = (I \in_{𝑔} J) ⊼_{𝑔} (K \in_{𝑔} n) \lor X = [\forall_{𝑔} K (I \in_{𝑔} J)])) \to \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (i \in_{𝑔} j)])$
39	2 3 4 12 38	syl31anc	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (i \in_{𝑔} j)])$
40	1	ovexi	$⊢ X \in V$
41		eqeq1	$⊢ x = X \to (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n))$
42	41	rexbidv	$⊢ x = X \to (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \leftrightarrow \exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n))$
43		eqeq1	$⊢ x = X \to (x = [\forall_{𝑔} k (i \in_{𝑔} j)] \leftrightarrow X = [\forall_{𝑔} k (i \in_{𝑔} j)])$
44	42 43	orbi12d	$⊢ x = X \to ((\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow (\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
45	44	rexbidv	$⊢ x = X \to (\exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow \exists k \in ω (\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
46	45	2rexbidv	$⊢ x = X \to (\exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
47	40 46	elab	$⊢ X \in \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\} \leftrightarrow \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω X = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor X = [\forall_{𝑔} k (i \in_{𝑔} j)])$
48	39 47	sylibr	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\}$
49	48	olcd	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to (X \in (\{\emptyset\} \times (ω \times ω)) \lor X \in \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\})$
50		elun	$⊢ X \in ((\{\emptyset\} \times (ω \times ω)) \cup \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\}) \leftrightarrow (X \in (\{\emptyset\} \times (ω \times ω)) \lor X \in \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\})$
51	49 50	sylibr	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in ((\{\emptyset\} \times (ω \times ω)) \cup \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\})$
52		fmla1	$⊢ Fmla (1_{𝑜}) = (\{\emptyset\} \times (ω \times ω)) \cup \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists n \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} n) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\}$
53	51 52	eleqtrrdi	$⊢ ((I \in ω \land J \in ω) \land (K \in ω \land L \in ω)) \to X \in Fmla (1_{𝑜})$

Metamath Proof Explorer

Theorem 2goelgoanfmla1

Proof