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

Theorem fmla0disjsuc 32876
 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 32860 . . . 4 (Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)}
2 rabab 3439 . . . 4 {𝑥 ∈ V ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} = {𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)}
31, 2eqtri 2781 . . 3 (Fmla‘∅) = {𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)}
43ineq1i 4113 . 2 ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})
5 inab 4203 . . 3 ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = {𝑥 ∣ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))}
6 goel 32825 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑗𝑔𝑘) = ⟨∅, ⟨𝑗, 𝑘⟩⟩)
76eqeq2d 2769 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) ↔ 𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩))
8 1n0 8129 . . . . . . . . . . . . . . . . . . . 20 1o ≠ ∅
98nesymi 3008 . . . . . . . . . . . . . . . . . . 19 ¬ ∅ = 1o
109intnanr 491 . . . . . . . . . . . . . . . . . 18 ¬ (∅ = 1o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑢, 𝑣⟩)
11 gonafv 32828 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ V ∧ 𝑣 ∈ V) → (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
1211el2v 3417 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩
1312eqeq2i 2771 . . . . . . . . . . . . . . . . . . 19 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣) ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
14 0ex 5177 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ V
15 opex 5324 . . . . . . . . . . . . . . . . . . . 20 𝑗, 𝑘⟩ ∈ V
1614, 15opth 5336 . . . . . . . . . . . . . . . . . . 19 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨1o, ⟨𝑢, 𝑣⟩⟩ ↔ (∅ = 1o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑢, 𝑣⟩))
1713, 16bitri 278 . . . . . . . . . . . . . . . . . 18 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣) ↔ (∅ = 1o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑢, 𝑣⟩))
1810, 17mtbir 326 . . . . . . . . . . . . . . . . 17 ¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣)
19 eqeq1 2762 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → (𝑥 = (𝑢𝑔𝑣) ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = (𝑢𝑔𝑣)))
2018, 19mtbiri 330 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → ¬ 𝑥 = (𝑢𝑔𝑣))
217, 20syl6bi 256 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) → ¬ 𝑥 = (𝑢𝑔𝑣)))
2221imp 410 . . . . . . . . . . . . . 14 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ¬ 𝑥 = (𝑢𝑔𝑣))
2322adantr 484 . . . . . . . . . . . . 13 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ¬ 𝑥 = (𝑢𝑔𝑣))
2423ralrimivw 3114 . . . . . . . . . . . 12 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣))
25 2on0 8123 . . . . . . . . . . . . . . . . . . . . 21 2o ≠ ∅
2625nesymi 3008 . . . . . . . . . . . . . . . . . . . 20 ¬ ∅ = 2o
2726orci 862 . . . . . . . . . . . . . . . . . . 19 (¬ ∅ = 2o ∨ ¬ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩)
2814, 15opth 5336 . . . . . . . . . . . . . . . . . . . . 21 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩ ↔ (∅ = 2o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
2928notbii 323 . . . . . . . . . . . . . . . . . . . 20 (¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩ ↔ ¬ (∅ = 2o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
30 ianor 979 . . . . . . . . . . . . . . . . . . . 20 (¬ (∅ = 2o ∧ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩) ↔ (¬ ∅ = 2o ∨ ¬ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
3129, 30bitri 278 . . . . . . . . . . . . . . . . . . 19 (¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩ ↔ (¬ ∅ = 2o ∨ ¬ ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑢⟩))
3227, 31mpbir 234 . . . . . . . . . . . . . . . . . 18 ¬ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩
33 eqeq1 2762 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → (𝑥 = ∀𝑔𝑖𝑢 ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ∀𝑔𝑖𝑢))
34 df-goal 32820 . . . . . . . . . . . . . . . . . . . 20 𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
3534eqeq2i 2771 . . . . . . . . . . . . . . . . . . 19 (⟨∅, ⟨𝑗, 𝑘⟩⟩ = ∀𝑔𝑖𝑢 ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩)
3633, 35bitrdi 290 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → (𝑥 = ∀𝑔𝑖𝑢 ↔ ⟨∅, ⟨𝑗, 𝑘⟩⟩ = ⟨2o, ⟨𝑖, 𝑢⟩⟩))
3732, 36mtbiri 330 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨∅, ⟨𝑗, 𝑘⟩⟩ → ¬ 𝑥 = ∀𝑔𝑖𝑢)
387, 37syl6bi 256 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) → ¬ 𝑥 = ∀𝑔𝑖𝑢))
3938imp 410 . . . . . . . . . . . . . . 15 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ¬ 𝑥 = ∀𝑔𝑖𝑢)
4039adantr 484 . . . . . . . . . . . . . 14 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ¬ 𝑥 = ∀𝑔𝑖𝑢)
4140adantr 484 . . . . . . . . . . . . 13 (((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) ∧ 𝑖 ∈ ω) → ¬ 𝑥 = ∀𝑔𝑖𝑢)
4241ralrimiva 3113 . . . . . . . . . . . 12 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢)
4324, 42jca 515 . . . . . . . . . . 11 ((((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) ∧ 𝑢 ∈ (Fmla‘∅)) → (∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢))
4443ralrimiva 3113 . . . . . . . . . 10 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ∀𝑢 ∈ (Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢))
45 ralnex 3163 . . . . . . . . . . . . . 14 (∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ↔ ¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣))
46 ralnex 3163 . . . . . . . . . . . . . 14 (∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢 ↔ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)
4745, 46anbi12i 629 . . . . . . . . . . . . 13 ((∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
48 ioran 981 . . . . . . . . . . . . 13 (¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
4947, 48bitr4i 281 . . . . . . . . . . . 12 ((∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5049ralbii 3097 . . . . . . . . . . 11 (∀𝑢 ∈ (Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ∀𝑢 ∈ (Fmla‘∅) ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
51 ralnex 3163 . . . . . . . . . . 11 (∀𝑢 ∈ (Fmla‘∅) ¬ (∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5250, 51bitri 278 . . . . . . . . . 10 (∀𝑢 ∈ (Fmla‘∅)(∀𝑣 ∈ (Fmla‘∅) ¬ 𝑥 = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ 𝑥 = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5344, 52sylib 221 . . . . . . . . 9 (((𝑗 ∈ ω ∧ 𝑘 ∈ ω) ∧ 𝑥 = (𝑗𝑔𝑘)) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5453ex 416 . . . . . . . 8 ((𝑗 ∈ ω ∧ 𝑘 ∈ ω) → (𝑥 = (𝑗𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
5554rexlimdva 3208 . . . . . . 7 (𝑗 ∈ ω → (∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
5655rexlimiv 3204 . . . . . 6 (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) → ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
5756imori 851 . . . . 5 (¬ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∨ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
58 ianor 979 . . . . 5 (¬ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) ↔ (¬ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∨ ¬ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))
5957, 58mpbir 234 . . . 4 ¬ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))
6059abf 4298 . . 3 {𝑥 ∣ (∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘) ∧ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))} = ∅
615, 60eqtri 2781 . 2 ({𝑥 ∣ ∃𝑗 ∈ ω ∃𝑘 ∈ ω 𝑥 = (𝑗𝑔𝑘)} ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅
624, 61eqtri 2781 1 ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cab 2735  ∀wral 3070  ∃wrex 3071  {crab 3074  Vcvv 3409   ∩ cin 3857  ∅c0 4225  ⟨cop 4528  ‘cfv 6335  (class class class)co 7150  ωcom 7579  1oc1o 8105  2oc2o 8106  ∈𝑔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-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:  satffunlem1lem2  32881
 Copyright terms: Public domain W3C validator