Theorem _nf_clos_neg ≪ | index | src | ≫

\nf闭包\neg（不可引用）

theorem _nf_clos_neg {x: set} (A: wff x): $ \nf x A $ > $ \nf x \neg A $;
StepHypRefExpression
1 iff_eliml 
(\nf x A \iff \nf x \neg A) \imp \nf x A \imp \nf x \neg A
2 iff_tran 
(\nf x A \iff \neg \fo x A \imp \fo x \neg A) \imp
  (\neg \fo x A \imp \fo x \neg A \iff \ex x \neg A \imp \fo x \neg A) \imp
  (\nf x A \iff \ex x \neg A \imp \fo x \neg A)
3 neg_imp_perm 
\neg \fo x \neg A \imp \fo x A \iff \neg \fo x A \imp \fo x \neg A
4 3 conv ex 
\ex x A \imp \fo x A \iff \neg \fo x A \imp \fo x \neg A
5 4 conv nf 
\nf x A \iff \neg \fo x A \imp \fo x \neg A
6 2, 5 ax_mp 
(\neg \fo x A \imp \fo x \neg A \iff \ex x \neg A \imp \fo x \neg A) \imp (\nf x A \iff \ex x \neg A \imp \fo x \neg A)
7 iff_intror_imp 
(\neg \fo x A \iff \ex x \neg A) \imp (\neg \fo x A \imp \fo x \neg A \iff \ex x \neg A \imp \fo x \neg A)
8 iff_symm 
(\ex x \neg A \iff \neg \fo x A) \imp (\neg \fo x A \iff \ex x \neg A)
9 exneg_eqv_negfo 
\ex x \neg A \iff \neg \fo x A
10 8, 9 ax_mp 
\neg \fo x A \iff \ex x \neg A
11 7, 10 ax_mp 
\neg \fo x A \imp \fo x \neg A \iff \ex x \neg A \imp \fo x \neg A
12 6, 11 ax_mp 
\nf x A \iff \ex x \neg A \imp \fo x \neg A
13 12 conv nf 
\nf x A \iff \nf x \neg A
14 1, 13 ax_mp 
\nf x A \imp \nf x \neg A
15 hyp h 
\nf x A
16 14, 15 ax_mp 
\nf x \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4)