fmla1

Description: The valid Godel formulas of height 1 is the set of all formulas of the form ( a |g b ) and A.g k a with atoms a , b of the form x e. y . (Contributed by AV, 20-Sep-2023)

		Ref	Expression
	Assertion	fmla1	$⊢ Fmla (1_{𝑜}) = (\{\emptyset\} \times (ω \times ω)) \cup \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\}$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
2	1	fveq2i	$⊢ Fmla (1_{𝑜}) = Fmla (suc \emptyset)$
3		peano1	$⊢ \emptyset \in ω$
4		fmlasuc	$⊢ \emptyset \in ω \to Fmla (suc \emptyset) = Fmla (\emptyset) \cup \{x \| \exists p \in Fmla (\emptyset) (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])\}$
5	3 4	ax-mp	$⊢ Fmla (suc \emptyset) = Fmla (\emptyset) \cup \{x \| \exists p \in Fmla (\emptyset) (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])\}$
6		fmla0xp	$⊢ Fmla (\emptyset) = \{\emptyset\} \times (ω \times ω)$
7		fmla0	$⊢ Fmla (\emptyset) = \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\}$
8	7	rexeqi	$⊢ \exists p \in Fmla (\emptyset) (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \leftrightarrow \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])$
9		eqeq1	$⊢ y = p \to (y = i \in_{𝑔} j \leftrightarrow p = i \in_{𝑔} j)$
10	9	2rexbidv	$⊢ y = p \to (\exists i \in ω \exists j \in ω y = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω p = i \in_{𝑔} j)$
11	10	elrab	$⊢ p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} \leftrightarrow (p \in V \land \exists i \in ω \exists j \in ω p = i \in_{𝑔} j)$
12		oveq1	$⊢ p = i \in_{𝑔} j \to p ⊼_{𝑔} q = (i \in_{𝑔} j) ⊼_{𝑔} q$
13	12	eqeq2d	$⊢ p = i \in_{𝑔} j \to (x = p ⊼_{𝑔} q \leftrightarrow x = (i \in_{𝑔} j) ⊼_{𝑔} q)$
14	13	rexbidv	$⊢ p = i \in_{𝑔} j \to (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \leftrightarrow \exists q \in Fmla (\emptyset) x = (i \in_{𝑔} j) ⊼_{𝑔} q)$
15		eqidd	$⊢ p = i \in_{𝑔} j \to k = k$
16		id	$⊢ p = i \in_{𝑔} j \to p = i \in_{𝑔} j$
17	15 16	goaleq12d	$⊢ p = i \in_{𝑔} j \to [\forall_{𝑔} k p] = [\forall_{𝑔} k (i \in_{𝑔} j)]$
18	17	eqeq2d	$⊢ p = i \in_{𝑔} j \to (x = [\forall_{𝑔} k p] \leftrightarrow x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
19	18	rexbidv	$⊢ p = i \in_{𝑔} j \to (\exists k \in ω x = [\forall_{𝑔} k p] \leftrightarrow \exists k \in ω x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
20	14 19	orbi12d	$⊢ p = i \in_{𝑔} j \to ((\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \leftrightarrow (\exists q \in Fmla (\emptyset) x = (i \in_{𝑔} j) ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
21		eqeq1	$⊢ z = q \to (z = k \in_{𝑔} l \leftrightarrow q = k \in_{𝑔} l)$
22	21	2rexbidv	$⊢ z = q \to (\exists k \in ω \exists l \in ω z = k \in_{𝑔} l \leftrightarrow \exists k \in ω \exists l \in ω q = k \in_{𝑔} l)$
23		fmla0	$⊢ Fmla (\emptyset) = \{z \in V \| \exists k \in ω \exists l \in ω z = k \in_{𝑔} l\}$
24	22 23	elrab2	$⊢ q \in Fmla (\emptyset) \leftrightarrow (q \in V \land \exists k \in ω \exists l \in ω q = k \in_{𝑔} l)$
25		oveq2	$⊢ q = k \in_{𝑔} l \to (i \in_{𝑔} j) ⊼_{𝑔} q = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l)$
26	25	eqeq2d	$⊢ q = k \in_{𝑔} l \to (x = (i \in_{𝑔} j) ⊼_{𝑔} q \leftrightarrow x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
27	26	biimpcd	$⊢ x = (i \in_{𝑔} j) ⊼_{𝑔} q \to (q = k \in_{𝑔} l \to x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
28	27	reximdv	$⊢ x = (i \in_{𝑔} j) ⊼_{𝑔} q \to (\exists l \in ω q = k \in_{𝑔} l \to \exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
29	28	reximdv	$⊢ x = (i \in_{𝑔} j) ⊼_{𝑔} q \to (\exists k \in ω \exists l \in ω q = k \in_{𝑔} l \to \exists k \in ω \exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
30	29	com12	$⊢ \exists k \in ω \exists l \in ω q = k \in_{𝑔} l \to (x = (i \in_{𝑔} j) ⊼_{𝑔} q \to \exists k \in ω \exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
31	24 30	simplbiim	$⊢ q \in Fmla (\emptyset) \to (x = (i \in_{𝑔} j) ⊼_{𝑔} q \to \exists k \in ω \exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
32	31	rexlimiv	$⊢ \exists q \in Fmla (\emptyset) x = (i \in_{𝑔} j) ⊼_{𝑔} q \to \exists k \in ω \exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l)$
33	32	orim1i	$⊢ (\exists q \in Fmla (\emptyset) x = (i \in_{𝑔} j) ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \to (\exists k \in ω \exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor \exists k \in ω x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
34		r19.43	$⊢ \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow (\exists k \in ω \exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor \exists k \in ω x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
35	33 34	sylibr	$⊢ (\exists q \in Fmla (\emptyset) x = (i \in_{𝑔} j) ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \to \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
36	20 35	syl6bi	$⊢ p = i \in_{𝑔} j \to ((\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \to \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
37	36	com12	$⊢ (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \to (p = i \in_{𝑔} j \to \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
38	37	reximdv	$⊢ (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \to (\exists j \in ω p = i \in_{𝑔} j \to \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
39	38	reximdv	$⊢ (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \to (\exists i \in ω \exists j \in ω p = i \in_{𝑔} j \to \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
40	39	com12	$⊢ \exists i \in ω \exists j \in ω p = i \in_{𝑔} j \to ((\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \to \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
41	11 40	simplbiim	$⊢ p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} \to ((\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \to \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]))$
42	41	rexlimiv	$⊢ \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \to \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
43		oveq1	$⊢ i = m \to i \in_{𝑔} j = m \in_{𝑔} j$
44	43	oveq1d	$⊢ i = m \to (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l)$
45	44	eqeq2d	$⊢ i = m \to (x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
46	45	rexbidv	$⊢ i = m \to (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow \exists l \in ω x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l))$
47		eqidd	$⊢ i = m \to k = k$
48	47 43	goaleq12d	$⊢ i = m \to [\forall_{𝑔} k (i \in_{𝑔} j)] = [\forall_{𝑔} k (m \in_{𝑔} j)]$
49	48	eqeq2d	$⊢ i = m \to (x = [\forall_{𝑔} k (i \in_{𝑔} j)] \leftrightarrow x = [\forall_{𝑔} k (m \in_{𝑔} j)])$
50	46 49	orbi12d	$⊢ i = m \to ((\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow (\exists l \in ω x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} j)]))$
51	50	rexbidv	$⊢ i = m \to (\exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow \exists k \in ω (\exists l \in ω x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} j)]))$
52		oveq2	$⊢ j = n \to m \in_{𝑔} j = m \in_{𝑔} n$
53	52	oveq1d	$⊢ j = n \to (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l)$
54	53	eqeq2d	$⊢ j = n \to (x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l))$
55	54	rexbidv	$⊢ j = n \to (\exists l \in ω x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow \exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l))$
56		eqidd	$⊢ j = n \to k = k$
57	56 52	goaleq12d	$⊢ j = n \to [\forall_{𝑔} k (m \in_{𝑔} j)] = [\forall_{𝑔} k (m \in_{𝑔} n)]$
58	57	eqeq2d	$⊢ j = n \to (x = [\forall_{𝑔} k (m \in_{𝑔} j)] \leftrightarrow x = [\forall_{𝑔} k (m \in_{𝑔} n)])$
59	55 58	orbi12d	$⊢ j = n \to ((\exists l \in ω x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} j)]) \leftrightarrow (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} n)]))$
60	59	rexbidv	$⊢ j = n \to (\exists k \in ω (\exists l \in ω x = (m \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} j)]) \leftrightarrow \exists k \in ω (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} n)]))$
61	51 60	cbvrex2vw	$⊢ \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \leftrightarrow \exists m \in ω \exists n \in ω \exists k \in ω (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} n)])$
62		oveq1	$⊢ k = o \to k \in_{𝑔} l = o \in_{𝑔} l$
63	62	oveq2d	$⊢ k = o \to (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l)$
64	63	eqeq2d	$⊢ k = o \to (x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l))$
65	64	rexbidv	$⊢ k = o \to (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \leftrightarrow \exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l))$
66		id	$⊢ k = o \to k = o$
67		eqidd	$⊢ k = o \to m \in_{𝑔} n = m \in_{𝑔} n$
68	66 67	goaleq12d	$⊢ k = o \to [\forall_{𝑔} k (m \in_{𝑔} n)] = [\forall_{𝑔} o (m \in_{𝑔} n)]$
69	68	eqeq2d	$⊢ k = o \to (x = [\forall_{𝑔} k (m \in_{𝑔} n)] \leftrightarrow x = [\forall_{𝑔} o (m \in_{𝑔} n)])$
70	65 69	orbi12d	$⊢ k = o \to ((\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} n)]) \leftrightarrow (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]))$
71	70	cbvrexvw	$⊢ \exists k \in ω (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} n)]) \leftrightarrow \exists o \in ω (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])$
72	3	ne0ii	$⊢ ω \neq \emptyset$
73		r19.44zv	$⊢ ω \neq \emptyset \to (\exists l \in ω (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \leftrightarrow (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]))$
74	72 73	ax-mp	$⊢ \exists l \in ω (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \leftrightarrow (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])$
75		eqeq1	$⊢ y = m \in_{𝑔} n \to (y = i \in_{𝑔} j \leftrightarrow m \in_{𝑔} n = i \in_{𝑔} j)$
76	75	2rexbidv	$⊢ y = m \in_{𝑔} n \to (\exists i \in ω \exists j \in ω y = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω m \in_{𝑔} n = i \in_{𝑔} j)$
77		ovexd	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])) \to m \in_{𝑔} n \in V$
78		simpl	$⊢ (m \in ω \land n \in ω) \to m \in ω$
79	43	eqeq2d	$⊢ i = m \to (m \in_{𝑔} n = i \in_{𝑔} j \leftrightarrow m \in_{𝑔} n = m \in_{𝑔} j)$
80	79	rexbidv	$⊢ i = m \to (\exists j \in ω m \in_{𝑔} n = i \in_{𝑔} j \leftrightarrow \exists j \in ω m \in_{𝑔} n = m \in_{𝑔} j)$
81	80	adantl	$⊢ ((m \in ω \land n \in ω) \land i = m) \to (\exists j \in ω m \in_{𝑔} n = i \in_{𝑔} j \leftrightarrow \exists j \in ω m \in_{𝑔} n = m \in_{𝑔} j)$
82		simpr	$⊢ (m \in ω \land n \in ω) \to n \in ω$
83	52	eqeq2d	$⊢ j = n \to (m \in_{𝑔} n = m \in_{𝑔} j \leftrightarrow m \in_{𝑔} n = m \in_{𝑔} n)$
84	83	adantl	$⊢ ((m \in ω \land n \in ω) \land j = n) \to (m \in_{𝑔} n = m \in_{𝑔} j \leftrightarrow m \in_{𝑔} n = m \in_{𝑔} n)$
85		eqidd	$⊢ (m \in ω \land n \in ω) \to m \in_{𝑔} n = m \in_{𝑔} n$
86	82 84 85	rspcedvd	$⊢ (m \in ω \land n \in ω) \to \exists j \in ω m \in_{𝑔} n = m \in_{𝑔} j$
87	78 81 86	rspcedvd	$⊢ (m \in ω \land n \in ω) \to \exists i \in ω \exists j \in ω m \in_{𝑔} n = i \in_{𝑔} j$
88	87	ad5ant12	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])) \to \exists i \in ω \exists j \in ω m \in_{𝑔} n = i \in_{𝑔} j$
89	76 77 88	elrabd	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])) \to m \in_{𝑔} n \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\}$
90		oveq1	$⊢ p = m \in_{𝑔} n \to p ⊼_{𝑔} q = (m \in_{𝑔} n) ⊼_{𝑔} q$
91	90	eqeq2d	$⊢ p = m \in_{𝑔} n \to (x = p ⊼_{𝑔} q \leftrightarrow x = (m \in_{𝑔} n) ⊼_{𝑔} q)$
92	91	rexbidv	$⊢ p = m \in_{𝑔} n \to (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \leftrightarrow \exists q \in Fmla (\emptyset) x = (m \in_{𝑔} n) ⊼_{𝑔} q)$
93		eqidd	$⊢ p = m \in_{𝑔} n \to k = k$
94		id	$⊢ p = m \in_{𝑔} n \to p = m \in_{𝑔} n$
95	93 94	goaleq12d	$⊢ p = m \in_{𝑔} n \to [\forall_{𝑔} k p] = [\forall_{𝑔} k (m \in_{𝑔} n)]$
96	95	eqeq2d	$⊢ p = m \in_{𝑔} n \to (x = [\forall_{𝑔} k p] \leftrightarrow x = [\forall_{𝑔} k (m \in_{𝑔} n)])$
97	96	rexbidv	$⊢ p = m \in_{𝑔} n \to (\exists k \in ω x = [\forall_{𝑔} k p] \leftrightarrow \exists k \in ω x = [\forall_{𝑔} k (m \in_{𝑔} n)])$
98	92 97	orbi12d	$⊢ p = m \in_{𝑔} n \to ((\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \leftrightarrow (\exists q \in Fmla (\emptyset) x = (m \in_{𝑔} n) ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k (m \in_{𝑔} n)]))$
99	98	adantl	$⊢ (((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])) \land p = m \in_{𝑔} n) \to ((\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \leftrightarrow (\exists q \in Fmla (\emptyset) x = (m \in_{𝑔} n) ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k (m \in_{𝑔} n)]))$
100		ovexd	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to o \in_{𝑔} l \in V$
101		simpr	$⊢ ((m \in ω \land n \in ω) \land o \in ω) \to o \in ω$
102	101	adantr	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to o \in ω$
103		oveq1	$⊢ i = o \to i \in_{𝑔} j = o \in_{𝑔} j$
104	103	eqeq2d	$⊢ i = o \to (o \in_{𝑔} l = i \in_{𝑔} j \leftrightarrow o \in_{𝑔} l = o \in_{𝑔} j)$
105	104	rexbidv	$⊢ i = o \to (\exists j \in ω o \in_{𝑔} l = i \in_{𝑔} j \leftrightarrow \exists j \in ω o \in_{𝑔} l = o \in_{𝑔} j)$
106	105	adantl	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land i = o) \to (\exists j \in ω o \in_{𝑔} l = i \in_{𝑔} j \leftrightarrow \exists j \in ω o \in_{𝑔} l = o \in_{𝑔} j)$
107		simpr	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to l \in ω$
108		oveq2	$⊢ j = l \to o \in_{𝑔} j = o \in_{𝑔} l$
109	108	eqeq2d	$⊢ j = l \to (o \in_{𝑔} l = o \in_{𝑔} j \leftrightarrow o \in_{𝑔} l = o \in_{𝑔} l)$
110	109	adantl	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land j = l) \to (o \in_{𝑔} l = o \in_{𝑔} j \leftrightarrow o \in_{𝑔} l = o \in_{𝑔} l)$
111		eqidd	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to o \in_{𝑔} l = o \in_{𝑔} l$
112	107 110 111	rspcedvd	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to \exists j \in ω o \in_{𝑔} l = o \in_{𝑔} j$
113	102 106 112	rspcedvd	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to \exists i \in ω \exists j \in ω o \in_{𝑔} l = i \in_{𝑔} j$
114		eqeq1	$⊢ p = o \in_{𝑔} l \to (p = i \in_{𝑔} j \leftrightarrow o \in_{𝑔} l = i \in_{𝑔} j)$
115	114	2rexbidv	$⊢ p = o \in_{𝑔} l \to (\exists i \in ω \exists j \in ω p = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω o \in_{𝑔} l = i \in_{𝑔} j)$
116		fmla0	$⊢ Fmla (\emptyset) = \{p \in V \| \exists i \in ω \exists j \in ω p = i \in_{𝑔} j\}$
117	115 116	elrab2	$⊢ o \in_{𝑔} l \in Fmla (\emptyset) \leftrightarrow (o \in_{𝑔} l \in V \land \exists i \in ω \exists j \in ω o \in_{𝑔} l = i \in_{𝑔} j)$
118	100 113 117	sylanbrc	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to o \in_{𝑔} l \in Fmla (\emptyset)$
119	118	adantr	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l)) \to o \in_{𝑔} l \in Fmla (\emptyset)$
120		oveq2	$⊢ q = o \in_{𝑔} l \to (m \in_{𝑔} n) ⊼_{𝑔} q = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l)$
121	120	eqeq2d	$⊢ q = o \in_{𝑔} l \to (x = (m \in_{𝑔} n) ⊼_{𝑔} q \leftrightarrow x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l))$
122	121	adantl	$⊢ (((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l)) \land q = o \in_{𝑔} l) \to (x = (m \in_{𝑔} n) ⊼_{𝑔} q \leftrightarrow x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l))$
123		simpr	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l)) \to x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l)$
124	119 122 123	rspcedvd	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l)) \to \exists q \in Fmla (\emptyset) x = (m \in_{𝑔} n) ⊼_{𝑔} q$
125	124	ex	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \to \exists q \in Fmla (\emptyset) x = (m \in_{𝑔} n) ⊼_{𝑔} q)$
126	102	adantr	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to o \in ω$
127	69	adantl	$⊢ (((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \land k = o) \to (x = [\forall_{𝑔} k (m \in_{𝑔} n)] \leftrightarrow x = [\forall_{𝑔} o (m \in_{𝑔} n)])$
128		simpr	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to x = [\forall_{𝑔} o (m \in_{𝑔} n)]$
129	126 127 128	rspcedvd	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to \exists k \in ω x = [\forall_{𝑔} k (m \in_{𝑔} n)]$
130	129	ex	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to (x = [\forall_{𝑔} o (m \in_{𝑔} n)] \to \exists k \in ω x = [\forall_{𝑔} k (m \in_{𝑔} n)])$
131	125 130	orim12d	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to ((x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to (\exists q \in Fmla (\emptyset) x = (m \in_{𝑔} n) ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k (m \in_{𝑔} n)]))$
132	131	imp	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])) \to (\exists q \in Fmla (\emptyset) x = (m \in_{𝑔} n) ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k (m \in_{𝑔} n)])$
133	89 99 132	rspcedvd	$⊢ ((((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \land (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)])) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])$
134	133	ex	$⊢ (((m \in ω \land n \in ω) \land o \in ω) \land l \in ω) \to ((x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]))$
135	134	rexlimdva	$⊢ ((m \in ω \land n \in ω) \land o \in ω) \to (\exists l \in ω (x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]))$
136	74 135	syl5bir	$⊢ ((m \in ω \land n \in ω) \land o \in ω) \to ((\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]))$
137	136	rexlimdva	$⊢ (m \in ω \land n \in ω) \to (\exists o \in ω (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (o \in_{𝑔} l) \lor x = [\forall_{𝑔} o (m \in_{𝑔} n)]) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]))$
138	71 137	syl5bi	$⊢ (m \in ω \land n \in ω) \to (\exists k \in ω (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} n)]) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]))$
139	138	rexlimivv	$⊢ \exists m \in ω \exists n \in ω \exists k \in ω (\exists l \in ω x = (m \in_{𝑔} n) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (m \in_{𝑔} n)]) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])$
140	61 139	sylbi	$⊢ \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)]) \to \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])$
141	42 140	impbii	$⊢ \exists p \in \{y \in V \| \exists i \in ω \exists j \in ω y = i \in_{𝑔} j\} (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \leftrightarrow \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
142	8 141	bitri	$⊢ \exists p \in Fmla (\emptyset) (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p]) \leftrightarrow \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])$
143	142	abbii	$⊢ \{x \| \exists p \in Fmla (\emptyset) (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])\} = \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\}$
144	6 143	uneq12i	$⊢ Fmla (\emptyset) \cup \{x \| \exists p \in Fmla (\emptyset) (\exists q \in Fmla (\emptyset) x = p ⊼_{𝑔} q \lor \exists k \in ω x = [\forall_{𝑔} k p])\} = (\{\emptyset\} \times (ω \times ω)) \cup \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\}$
145	2 5 144	3eqtri	$⊢ Fmla (1_{𝑜}) = (\{\emptyset\} \times (ω \times ω)) \cup \{x \| \exists i \in ω \exists j \in ω \exists k \in ω (\exists l \in ω x = (i \in_{𝑔} j) ⊼_{𝑔} (k \in_{𝑔} l) \lor x = [\forall_{𝑔} k (i \in_{𝑔} j)])\}$

Metamath Proof Explorer

Theorem fmla1

Proof