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 ) )