Theorem fmla0xp

Description: The valid Godel formulas of height 0 is the set of all formulas of the form v_i e. v_j ("Godel-set of membership") coded as <. (/) , <. i , j >. >. . (Contributed by AV, 15-Sep-2023)

	Ref	Expression
Assertion	fmla0xp	⊢ ( Fmla ‘ ∅ ) = ( { ∅ } × ( ω × ω ) )

Proof

Step	Hyp	Ref	Expression
1		fmla0	⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) }
2		rabab	⊢ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) }
3		abeq1	⊢ ( { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } = ( { ∅ } × ( ω × ω ) ) ↔ ∀ 𝑥 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) ) )
4		goel	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
5	4	eqeq2d	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
6	5	2rexbiia	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
7		0ex	⊢ ∅ ∈ V
8	7	snid	⊢ ∅ ∈ { ∅ }
9	8	a1i	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ∅ ∈ { ∅ } )
10		opelxpi	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ω × ω ) )
11	9 10	opelxpd	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( { ∅ } × ( ω × ω ) ) )
12		eleq1	⊢ ( 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) ↔ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( { ∅ } × ( ω × ω ) ) ) )
13	11 12	syl5ibrcom	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) ) )
14	13	rexlimivv	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) )
15		elxpi	⊢ ( 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) → ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) ) )
16		elsni	⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
17	16	opeq1d	⊢ ( 𝑦 ∈ { ∅ } → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ ∅ , 𝑧 ⟩ )
18	17	eqeq2d	⊢ ( 𝑦 ∈ { ∅ } → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ↔ 𝑥 = ⟨ ∅ , 𝑧 ⟩ ) )
19	18	adantr	⊢ ( ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ↔ 𝑥 = ⟨ ∅ , 𝑧 ⟩ ) )
20		elxpi	⊢ ( 𝑧 ∈ ( ω × ω ) → ∃ 𝑖 ∃ 𝑗 ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) )
21		simprr	⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) )
22		simpl	⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → 𝑥 = ⟨ ∅ , 𝑧 ⟩ )
23		opeq2	⊢ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
24	23	adantr	⊢ ( ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
25	24	adantl	⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
26	22 25	eqtrd	⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
27	21 26	jca	⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
28	27	ex	⊢ ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ( ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) )
29	28	2eximdv	⊢ ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ( ∃ 𝑖 ∃ 𝑗 ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) )
30		r2ex	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
31	29 30	syl6ibr	⊢ ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ( ∃ 𝑖 ∃ 𝑗 ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
32	20 31	syl5com	⊢ ( 𝑧 ∈ ( ω × ω ) → ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
33	32	adantl	⊢ ( ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) → ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
34	19 33	sylbid	⊢ ( ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
35	34	impcom	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
36	35	exlimivv	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
37	15 36	syl	⊢ ( 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
38	14 37	impbii	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) )
39	6 38	bitri	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) )
40	3 39	mpgbir	⊢ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } = ( { ∅ } × ( ω × ω ) )
41	1 2 40	3eqtri	⊢ ( Fmla ‘ ∅ ) = ( { ∅ } × ( ω × ω ) )