Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gonar Structured version   Visualization version   GIF version

Theorem gonar 32873
 Description: If the "Godel-set of NAND" applied to classes is a Godel formula, the classes are also Godel formulas. Remark: The reverse is not valid for 𝐴 or 𝐵 being of the same height as the "Godel-set of NAND". (Contributed by AV, 21-Oct-2023.)
Assertion
Ref Expression
gonar ((𝑁 ∈ ω ∧ (𝑎𝑔𝑏) ∈ (Fmla‘𝑁)) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)))
Distinct variable group:   𝑎,𝑏
Allowed substitution hints:   𝑁(𝑎,𝑏)

Proof of Theorem gonar
Dummy variables 𝑖 𝑗 𝑥 𝑢 𝑣 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gonan0 32870 . . 3 ((𝑎𝑔𝑏) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅)
21adantl 485 . 2 ((𝑁 ∈ ω ∧ (𝑎𝑔𝑏) ∈ (Fmla‘𝑁)) → 𝑁 ≠ ∅)
3 nnsuc 7596 . . . 4 ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → ∃𝑥 ∈ ω 𝑁 = suc 𝑥)
4 suceq 6234 . . . . . . . . . . 11 (𝑑 = ∅ → suc 𝑑 = suc ∅)
54fveq2d 6662 . . . . . . . . . 10 (𝑑 = ∅ → (Fmla‘suc 𝑑) = (Fmla‘suc ∅))
65eleq2d 2837 . . . . . . . . 9 (𝑑 = ∅ → ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎𝑔𝑏) ∈ (Fmla‘suc ∅)))
75eleq2d 2837 . . . . . . . . . 10 (𝑑 = ∅ → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc ∅)))
85eleq2d 2837 . . . . . . . . . 10 (𝑑 = ∅ → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc ∅)))
97, 8anbi12d 633 . . . . . . . . 9 (𝑑 = ∅ → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
106, 9imbi12d 348 . . . . . . . 8 (𝑑 = ∅ → (((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘suc ∅) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))))
11 suceq 6234 . . . . . . . . . . 11 (𝑑 = 𝑐 → suc 𝑑 = suc 𝑐)
1211fveq2d 6662 . . . . . . . . . 10 (𝑑 = 𝑐 → (Fmla‘suc 𝑑) = (Fmla‘suc 𝑐))
1312eleq2d 2837 . . . . . . . . 9 (𝑑 = 𝑐 → ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑐)))
1412eleq2d 2837 . . . . . . . . . 10 (𝑑 = 𝑐 → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc 𝑐)))
1512eleq2d 2837 . . . . . . . . . 10 (𝑑 = 𝑐 → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc 𝑐)))
1614, 15anbi12d 633 . . . . . . . . 9 (𝑑 = 𝑐 → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc 𝑐))))
1713, 16imbi12d 348 . . . . . . . 8 (𝑑 = 𝑐 → (((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑐) → (𝑎 ∈ (Fmla‘suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc 𝑐)))))
18 suceq 6234 . . . . . . . . . . 11 (𝑑 = suc 𝑐 → suc 𝑑 = suc suc 𝑐)
1918fveq2d 6662 . . . . . . . . . 10 (𝑑 = suc 𝑐 → (Fmla‘suc 𝑑) = (Fmla‘suc suc 𝑐))
2019eleq2d 2837 . . . . . . . . 9 (𝑑 = suc 𝑐 → ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎𝑔𝑏) ∈ (Fmla‘suc suc 𝑐)))
2119eleq2d 2837 . . . . . . . . . 10 (𝑑 = suc 𝑐 → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc suc 𝑐)))
2219eleq2d 2837 . . . . . . . . . 10 (𝑑 = suc 𝑐 → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc suc 𝑐)))
2321, 22anbi12d 633 . . . . . . . . 9 (𝑑 = suc 𝑐 → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑐))))
2420, 23imbi12d 348 . . . . . . . 8 (𝑑 = suc 𝑐 → (((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘suc suc 𝑐) → (𝑎 ∈ (Fmla‘suc suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑐)))))
25 suceq 6234 . . . . . . . . . . 11 (𝑑 = 𝑥 → suc 𝑑 = suc 𝑥)
2625fveq2d 6662 . . . . . . . . . 10 (𝑑 = 𝑥 → (Fmla‘suc 𝑑) = (Fmla‘suc 𝑥))
2726eleq2d 2837 . . . . . . . . 9 (𝑑 = 𝑥 → ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑥)))
2826eleq2d 2837 . . . . . . . . . 10 (𝑑 = 𝑥 → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc 𝑥)))
2926eleq2d 2837 . . . . . . . . . 10 (𝑑 = 𝑥 → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc 𝑥)))
3028, 29anbi12d 633 . . . . . . . . 9 (𝑑 = 𝑥 → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥))))
3127, 30imbi12d 348 . . . . . . . 8 (𝑑 = 𝑥 → (((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥)))))
32 peano1 7600 . . . . . . . . . 10 ∅ ∈ ω
33 ovex 7183 . . . . . . . . . 10 (𝑎𝑔𝑏) ∈ V
34 isfmlasuc 32866 . . . . . . . . . 10 ((∅ ∈ ω ∧ (𝑎𝑔𝑏) ∈ V) → ((𝑎𝑔𝑏) ∈ (Fmla‘suc ∅) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘∅) ∨ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎𝑔𝑏) = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎𝑔𝑏) = ∀𝑔𝑖𝑢))))
3532, 33, 34mp2an 691 . . . . . . . . 9 ((𝑎𝑔𝑏) ∈ (Fmla‘suc ∅) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘∅) ∨ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎𝑔𝑏) = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎𝑔𝑏) = ∀𝑔𝑖𝑢)))
36 eqeq1 2762 . . . . . . . . . . . . 13 (𝑥 = (𝑎𝑔𝑏) → (𝑥 = (𝑖𝑔𝑗) ↔ (𝑎𝑔𝑏) = (𝑖𝑔𝑗)))
37362rexbidv 3224 . . . . . . . . . . . 12 (𝑥 = (𝑎𝑔𝑏) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑎𝑔𝑏) = (𝑖𝑔𝑗)))
38 fmla0 32860 . . . . . . . . . . . 12 (Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)}
3937, 38elrab2 3605 . . . . . . . . . . 11 ((𝑎𝑔𝑏) ∈ (Fmla‘∅) ↔ ((𝑎𝑔𝑏) ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑎𝑔𝑏) = (𝑖𝑔𝑗)))
40 gonafv 32828 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
4140el2v 3417 . . . . . . . . . . . . . . . . 17 (𝑎𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩
4241a1i 11 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑎𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
43 goel 32825 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖𝑔𝑗) = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
4442, 43eqeq12d 2774 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑎𝑔𝑏) = (𝑖𝑔𝑗) ↔ ⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨∅, ⟨𝑖, 𝑗⟩⟩))
45 1oex 8120 . . . . . . . . . . . . . . . . 17 1o ∈ V
46 opex 5324 . . . . . . . . . . . . . . . . 17 𝑎, 𝑏⟩ ∈ V
4745, 46opth 5336 . . . . . . . . . . . . . . . 16 (⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨∅, ⟨𝑖, 𝑗⟩⟩ ↔ (1o = ∅ ∧ ⟨𝑎, 𝑏⟩ = ⟨𝑖, 𝑗⟩))
48 1n0 8129 . . . . . . . . . . . . . . . . . 18 1o ≠ ∅
49 eqneqall 2962 . . . . . . . . . . . . . . . . . 18 (1o = ∅ → (1o ≠ ∅ → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
5048, 49mpi 20 . . . . . . . . . . . . . . . . 17 (1o = ∅ → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
5150adantr 484 . . . . . . . . . . . . . . . 16 ((1o = ∅ ∧ ⟨𝑎, 𝑏⟩ = ⟨𝑖, 𝑗⟩) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
5247, 51sylbi 220 . . . . . . . . . . . . . . 15 (⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
5344, 52syl6bi 256 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑎𝑔𝑏) = (𝑖𝑔𝑗) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
5453rexlimdva 3208 . . . . . . . . . . . . 13 (𝑖 ∈ ω → (∃𝑗 ∈ ω (𝑎𝑔𝑏) = (𝑖𝑔𝑗) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
5554rexlimiv 3204 . . . . . . . . . . . 12 (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑎𝑔𝑏) = (𝑖𝑔𝑗) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
5655adantl 485 . . . . . . . . . . 11 (((𝑎𝑔𝑏) ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑎𝑔𝑏) = (𝑖𝑔𝑗)) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
5739, 56sylbi 220 . . . . . . . . . 10 ((𝑎𝑔𝑏) ∈ (Fmla‘∅) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
5841a1i 11 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) → (𝑎𝑔𝑏) = ⟨1o, ⟨𝑎, 𝑏⟩⟩)
59 gonafv 32828 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) → (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
6058, 59eqeq12d 2774 . . . . . . . . . . . . . 14 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) → ((𝑎𝑔𝑏) = (𝑢𝑔𝑣) ↔ ⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩))
6145, 46opth 5336 . . . . . . . . . . . . . . . . 17 (⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩ ↔ (1o = 1o ∧ ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑣⟩))
62 vex 3413 . . . . . . . . . . . . . . . . . . . 20 𝑎 ∈ V
63 vex 3413 . . . . . . . . . . . . . . . . . . . 20 𝑏 ∈ V
6462, 63opth 5336 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑣⟩ ↔ (𝑎 = 𝑢𝑏 = 𝑣))
65 simpl 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑎 = 𝑢)
6665equcomd 2026 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑢 = 𝑎)
6766eleq1d 2836 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑢 ∈ (Fmla‘∅) ↔ 𝑎 ∈ (Fmla‘∅)))
68 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑏 = 𝑣)
6968equcomd 2026 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑣 = 𝑏)
7069eleq1d 2836 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑣 ∈ (Fmla‘∅) ↔ 𝑏 ∈ (Fmla‘∅)))
7167, 70anbi12d 633 . . . . . . . . . . . . . . . . . . 19 ((𝑎 = 𝑢𝑏 = 𝑣) → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) ↔ (𝑎 ∈ (Fmla‘∅) ∧ 𝑏 ∈ (Fmla‘∅))))
7264, 71sylbi 220 . . . . . . . . . . . . . . . . . 18 (⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑣⟩ → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) ↔ (𝑎 ∈ (Fmla‘∅) ∧ 𝑏 ∈ (Fmla‘∅))))
7372adantl 485 . . . . . . . . . . . . . . . . 17 ((1o = 1o ∧ ⟨𝑎, 𝑏⟩ = ⟨𝑢, 𝑣⟩) → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) ↔ (𝑎 ∈ (Fmla‘∅) ∧ 𝑏 ∈ (Fmla‘∅))))
7461, 73sylbi 220 . . . . . . . . . . . . . . . 16 (⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩ → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) ↔ (𝑎 ∈ (Fmla‘∅) ∧ 𝑏 ∈ (Fmla‘∅))))
75 fmlasssuc 32867 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ ω → (Fmla‘∅) ⊆ (Fmla‘suc ∅))
7632, 75ax-mp 5 . . . . . . . . . . . . . . . . . 18 (Fmla‘∅) ⊆ (Fmla‘suc ∅)
7776sseli 3888 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc ∅))
7876sseli 3888 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (Fmla‘∅) → 𝑏 ∈ (Fmla‘suc ∅))
7977, 78anim12i 615 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ (Fmla‘∅) ∧ 𝑏 ∈ (Fmla‘∅)) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
8074, 79syl6bi 256 . . . . . . . . . . . . . . 15 (⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩ → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
8180com12 32 . . . . . . . . . . . . . 14 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) → (⟨1o, ⟨𝑎, 𝑏⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩ → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
8260, 81sylbid 243 . . . . . . . . . . . . 13 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) → ((𝑎𝑔𝑏) = (𝑢𝑔𝑣) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
8382rexlimdva 3208 . . . . . . . . . . . 12 (𝑢 ∈ (Fmla‘∅) → (∃𝑣 ∈ (Fmla‘∅)(𝑎𝑔𝑏) = (𝑢𝑔𝑣) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
84 gonanegoal 32830 . . . . . . . . . . . . . . 15 (𝑎𝑔𝑏) ≠ ∀𝑔𝑖𝑢
85 eqneqall 2962 . . . . . . . . . . . . . . 15 ((𝑎𝑔𝑏) = ∀𝑔𝑖𝑢 → ((𝑎𝑔𝑏) ≠ ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
8684, 85mpi 20 . . . . . . . . . . . . . 14 ((𝑎𝑔𝑏) = ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
8786a1i 11 . . . . . . . . . . . . 13 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑖 ∈ ω) → ((𝑎𝑔𝑏) = ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
8887rexlimdva 3208 . . . . . . . . . . . 12 (𝑢 ∈ (Fmla‘∅) → (∃𝑖 ∈ ω (𝑎𝑔𝑏) = ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
8983, 88jaod 856 . . . . . . . . . . 11 (𝑢 ∈ (Fmla‘∅) → ((∃𝑣 ∈ (Fmla‘∅)(𝑎𝑔𝑏) = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎𝑔𝑏) = ∀𝑔𝑖𝑢) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅))))
9089rexlimiv 3204 . . . . . . . . . 10 (∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎𝑔𝑏) = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎𝑔𝑏) = ∀𝑔𝑖𝑢) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
9157, 90jaoi 854 . . . . . . . . 9 (((𝑎𝑔𝑏) ∈ (Fmla‘∅) ∨ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎𝑔𝑏) = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎𝑔𝑏) = ∀𝑔𝑖𝑢)) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
9235, 91sylbi 220 . . . . . . . 8 ((𝑎𝑔𝑏) ∈ (Fmla‘suc ∅) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc ∅)))
93 gonarlem 32872 . . . . . . . 8 (𝑐 ∈ ω → (((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑐) → (𝑎 ∈ (Fmla‘suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc 𝑐))) → ((𝑎𝑔𝑏) ∈ (Fmla‘suc suc 𝑐) → (𝑎 ∈ (Fmla‘suc suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑐)))))
9410, 17, 24, 31, 92, 93finds 7608 . . . . . . 7 (𝑥 ∈ ω → ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥))))
9594adantr 484 . . . . . 6 ((𝑥 ∈ ω ∧ 𝑁 = suc 𝑥) → ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥))))
96 fveq2 6658 . . . . . . . . 9 (𝑁 = suc 𝑥 → (Fmla‘𝑁) = (Fmla‘suc 𝑥))
9796eleq2d 2837 . . . . . . . 8 (𝑁 = suc 𝑥 → ((𝑎𝑔𝑏) ∈ (Fmla‘𝑁) ↔ (𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑥)))
9896eleq2d 2837 . . . . . . . . 9 (𝑁 = suc 𝑥 → (𝑎 ∈ (Fmla‘𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑥)))
9996eleq2d 2837 . . . . . . . . 9 (𝑁 = suc 𝑥 → (𝑏 ∈ (Fmla‘𝑁) ↔ 𝑏 ∈ (Fmla‘suc 𝑥)))
10098, 99anbi12d 633 . . . . . . . 8 (𝑁 = suc 𝑥 → ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)) ↔ (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥))))
10197, 100imbi12d 348 . . . . . . 7 (𝑁 = suc 𝑥 → (((𝑎𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥)))))
102101adantl 485 . . . . . 6 ((𝑥 ∈ ω ∧ 𝑁 = suc 𝑥) → (((𝑎𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))) ↔ ((𝑎𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥)))))
10395, 102mpbird 260 . . . . 5 ((𝑥 ∈ ω ∧ 𝑁 = suc 𝑥) → ((𝑎𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))))
104103rexlimiva 3205 . . . 4 (∃𝑥 ∈ ω 𝑁 = suc 𝑥 → ((𝑎𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))))
1053, 104syl 17 . . 3 ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → ((𝑎𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))))
106105impancom 455 . 2 ((𝑁 ∈ ω ∧ (𝑎𝑔𝑏) ∈ (Fmla‘𝑁)) → (𝑁 ≠ ∅ → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))))
1072, 106mpd 15 1 ((𝑁 ∈ ω ∧ (𝑎𝑔𝑏) ∈ (Fmla‘𝑁)) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∃wrex 3071  Vcvv 3409   ⊆ wss 3858  ∅c0 4225  ⟨cop 4528  suc csuc 6171  ‘cfv 6335  (class class class)co 7150  ωcom 7579  1oc1o 8105  ∈𝑔cgoe 32811  ⊼𝑔cgna 32812  ∀𝑔cgol 32813  Fmlacfmla 32815 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-map 8418  df-goel 32818  df-gona 32819  df-goal 32820  df-sat 32821  df-fmla 32823 This theorem is referenced by:  fmlasucdisj  32877
 Copyright terms: Public domain W3C validator