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

Theorem fmla0disjsuc 34327
Description: The set of valid Godel formulas of height 0 is disjoint with the formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification. (Contributed by AV, 20-Oct-2023.)
Assertion
Ref Expression
fmla0disjsuc ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅
Distinct variable group:   𝑢,𝑖,𝑣,𝑥

Proof of Theorem fmla0disjsuc
Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmla0 34311 . . . 4 (Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)}
2 rabab 3503 . . . 4 {𝑥 ∈ V ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} = {𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)}
31, 2eqtri 2761 . . 3 (Fmla‘∅) = {𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)}
43ineq1i 4207 . 2 ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})
5 inab 4298 . . 3 ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = {𝑥 ∣ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))}
6 goel 34276 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑗𝑔𝑘) = ⟨∅, ⟨𝑗, 𝑘⟩⟩)
76eqeq2d 2744 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) ↔ 𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩))
8 1n0 8483 . . . . . . . . . . . . . . . . . . . 20 1o ≠ ∅
98nesymi 2999 . . . . . . . . . . . . . . . . . . 19 ¬ ∅ = 1o
109intnanr 489 . . . . . . . . . . . . . . . . . 18 ¬ (∅ = 1o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑢, 𝑣⟩)
11 gonafv 34279 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
1211el2v 3483 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩
1312eqeq2i 2746 . . . . . . . . . . . . . . . . . . 19 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣) ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
14 0ex 5306 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ V
15 opex 5463 . . . . . . . . . . . . . . . . . . . 20 𝑗, 𝑘⟩ ∈ V
1614, 15opth 5475 . . . . . . . . . . . . . . . . . . 19 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩ ↔ (∅ = 1o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑢, 𝑣⟩))
1713, 16bitri 275 . . . . . . . . . . . . . . . . . 18 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣) ↔ (∅ = 1o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑢, 𝑣⟩))
1810, 17mtbir 323 . . . . . . . . . . . . . . . . 17 ¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣)
19 eqeq1 2737 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → (𝑥 = (𝑢𝑔𝑣) ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣)))
2018, 19mtbiri 327 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → ¬ 𝑥 = (𝑢𝑔𝑣))
217, 20syl6bi 253 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) → ¬ 𝑥 = (𝑢𝑔𝑣)))
2221imp 408 . . . . . . . . . . . . . 14 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ¬ 𝑥 = (𝑢𝑔𝑣))
2322adantr 482 . . . . . . . . . . . . 13 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ¬ 𝑥 = (𝑢𝑔𝑣))
2423ralrimivw 3151 . . . . . . . . . . . 12 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣))
25 2on0 8477 . . . . . . . . . . . . . . . . . . . . 21 2o ≠ ∅
2625nesymi 2999 . . . . . . . . . . . . . . . . . . . 20 ¬ ∅ = 2o
2726orci 864 . . . . . . . . . . . . . . . . . . 19 (¬ ∅ = 2o ∨ ¬ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩)
2814, 15opth 5475 . . . . . . . . . . . . . . . . . . . . 21 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩ ↔ (∅ = 2o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
2928notbii 320 . . . . . . . . . . . . . . . . . . . 20 (¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩ ↔ ¬ (∅ = 2o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
30 ianor 981 . . . . . . . . . . . . . . . . . . . 20 (¬ (∅ = 2o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩) ↔ (¬ ∅ = 2o ∨ ¬ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
3129, 30bitri 275 . . . . . . . . . . . . . . . . . . 19 (¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩ ↔ (¬ ∅ = 2o ∨ ¬ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
3227, 31mpbir 230 . . . . . . . . . . . . . . . . . 18 ¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩
33 eqeq1 2737 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → (𝑥 = ∀𝑔𝑖𝑢 ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ∀𝑔𝑖𝑢))
34 df-goal 34271 . . . . . . . . . . . . . . . . . . . 20 𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
3534eqeq2i 2746 . . . . . . . . . . . . . . . . . . 19 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = ∀𝑔𝑖𝑢 ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩)
3633, 35bitrdi 287 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → (𝑥 = ∀𝑔𝑖𝑢 ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩))
3732, 36mtbiri 327 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → ¬ 𝑥 = ∀𝑔𝑖𝑢)
387, 37syl6bi 253 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) → ¬ 𝑥 = ∀𝑔𝑖𝑢))
3938imp 408 . . . . . . . . . . . . . . 15 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ¬ 𝑥 = ∀𝑔𝑖𝑢)
4039adantr 482 . . . . . . . . . . . . . 14 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ¬ 𝑥 = ∀𝑔𝑖𝑢)
4140adantr 482 . . . . . . . . . . . . 13 (((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) ∧ 𝑖 ∈ ω) → ¬ 𝑥 = ∀𝑔𝑖𝑢)
4241ralrimiva 3147 . . . . . . . . . . . 12 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢)
4324, 42jca 513 . . . . . . . . . . 11 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → (∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢))
4443ralrimiva 3147 . . . . . . . . . 10 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ∀𝑢 ∈ (Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢))
45 ralnex 3073 . . . . . . . . . . . . . 14 (∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ↔ ¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣))
46 ralnex 3073 . . . . . . . . . . . . . 14 (∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢 ↔ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)
4745, 46anbi12i 628 . . . . . . . . . . . . 13 ((∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
48 ioran 983 . . . . . . . . . . . . 13 (¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
4947, 48bitr4i 278 . . . . . . . . . . . 12 ((∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5049ralbii 3094 . . . . . . . . . . 11 (∀𝑢 ∈ (Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ∀𝑢 ∈ (Fmla‘∅) ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
51 ralnex 3073 . . . . . . . . . . 11 (∀𝑢 ∈ (Fmla‘∅) ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5250, 51bitri 275 . . . . . . . . . 10 (∀𝑢 ∈ (Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5344, 52sylib 217 . . . . . . . . 9 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5453ex 414 . . . . . . . 8 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
5554rexlimdva 3156 . . . . . . 7 (𝑗 ∈ ω → (∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
5655rexlimiv 3149 . . . . . 6 (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5756imori 853 . . . . 5 (¬ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∨ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
58 ianor 981 . . . . 5 (¬ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) ↔ (¬ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∨ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
5957, 58mpbir 230 . . . 4 ¬ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
6059abf 4401 . . 3 {𝑥 ∣ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))} = ∅
615, 60eqtri 2761 . 2 ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅
624, 61eqtri 2761 1 ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 397  wo 846   = wceq 1542  wcel 2107  {cab 2710  wral 3062  wrex 3071  {crab 3433  Vcvv 3475  cin 3946  c0 4321  cop 4633  cfv 6540  (class class class)co 7404  ωcom 7850  1oc1o 8454  2oc2o 8455  𝑔cgoe 34262  𝑔cgna 34263  𝑔cgol 34264  Fmlacfmla 34266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-map 8818  df-goel 34269  df-gona 34270  df-goal 34271  df-sat 34272  df-fmla 34274
This theorem is referenced by:  satffunlem1lem2  34332
  Copyright terms: Public domain W3C validator