This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) )
Assertion 2goelgoanfmla1 ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ ( Fmla ‘ 1o ) )

Proof

Step Hyp Ref Expression
1 satfv1fvfmla1.x ⊢ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) )
2 simpll ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐼 ∈ ω )
3 simplr ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐽 ∈ ω )
4 simprl ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐾 ∈ ω )
5 simprr ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐿 ∈ ω )
6 oveq2 ⊢ ( 𝑛 = 𝐿 → ( 𝐾 ∈𝑔 𝑛 ) = ( 𝐾 ∈𝑔 𝐿 ) )
7 6 oveq2d ⊢ ( 𝑛 = 𝐿 → ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) )
8 7 eqeq2d ⊢ ( 𝑛 = 𝐿 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ) )
9 8 adantl ⊢ ( ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑛 = 𝐿 ) → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ) )
10 1 a1i ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) )
11 5 9 10 rspcedvd ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) )
12 11 orcd ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) )
13 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∈𝑔 𝑗 ) = ( 𝐼 ∈𝑔 𝑗 ) )
14 13 oveq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) )
15 14 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) )
16 15 rexbidv ⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) )
17 eqidd ⊢ ( 𝑖 = 𝐼 → 𝑘 = 𝑘 )
18 17 13 goaleq12d ⊢ ( 𝑖 = 𝐼 → ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) )
19 18 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ) )
20 16 19 orbi12d ⊢ ( 𝑖 = 𝐼 → ( ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ) ) )
21 oveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐼 ∈𝑔 𝑗 ) = ( 𝐼 ∈𝑔 𝐽 ) )
22 21 oveq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) )
23 22 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) )
24 23 rexbidv ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) )
25 eqidd ⊢ ( 𝑗 = 𝐽 → 𝑘 = 𝑘 )
26 25 21 goaleq12d ⊢ ( 𝑗 = 𝐽 → ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) )
27 26 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ) )
28 24 27 orbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ) ) )
29 oveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ∈𝑔 𝑛 ) = ( 𝐾 ∈𝑔 𝑛 ) )
30 29 oveq2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) )
31 30 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ) )
32 31 rexbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ) )
33 id ⊢ ( 𝑘 = 𝐾 → 𝑘 = 𝐾 )
34 eqidd ⊢ ( 𝑘 = 𝐾 → ( 𝐼 ∈𝑔 𝐽 ) = ( 𝐼 ∈𝑔 𝐽 ) )
35 33 34 goaleq12d ⊢ ( 𝑘 = 𝐾 → ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) )
36 35 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ↔ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) )
37 32 36 orbi12d ⊢ ( 𝑘 = 𝐾 → ( ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) ) )
38 20 28 37 rspc3ev ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐾 ∈ ω ) ∧ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
39 2 3 4 12 38 syl31anc ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
40 1 ovexi ⊢ 𝑋 ∈ V
41 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) )
42 41 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) )
43 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
44 42 43 orbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
45 44 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
46 45 2rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) )
47 40 46 elab ⊢ ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) )
48 39 47 sylibr ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } )
49 48 olcd ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑋 ∈ ( { ∅ } × ( ω × ω ) ) ∨ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) )
50 elun ⊢ ( 𝑋 ∈ ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) ↔ ( 𝑋 ∈ ( { ∅ } × ( ω × ω ) ) ∨ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) )
51 49 50 sylibr ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) )
52 fmla1 ⊢ ( Fmla ‘ 1o ) = ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } )
53 51 52 eleqtrrdi ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ ( Fmla ‘ 1o ) )