\nf闭包\imp（不可引用）
theorem _nf_clos_imp {x: set} (A B: wff x):
$ \nf x A $ >
$ \nf x B $ >
$ \nf x (A \imp B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ex_imp_fo_extto_fo | (\ex x A \imp \fo x B) \imp \fo x (A \imp B) |
|
| 2 | 1 | _hyp_null_complete | \ex x (A \imp B) \imp (\ex x A \imp \fo x B) \imp \fo x (A \imp B) |
| 3 | imp_tran | (\ex x A \imp \ex x B) \imp (\ex x B \imp \fo x B) \imp \ex x A \imp \fo x B |
|
| 4 | 3 | _hyp_null_complete | \ex x (A \imp B) \imp (\ex x A \imp \ex x B) \imp (\ex x B \imp \fo x B) \imp \ex x A \imp \fo x B |
| 5 | imp_tran | (\ex x A \imp \fo x A) \imp (\fo x A \imp \ex x B) \imp \ex x A \imp \ex x B |
|
| 6 | 5 | _hyp_null_complete | \ex x (A \imp B) \imp (\ex x A \imp \fo x A) \imp (\fo x A \imp \ex x B) \imp \ex x A \imp \ex x B |
| 7 | hyp h1 | \nf x A |
|
| 8 | 7 | conv nf | \ex x A \imp \fo x A |
| 9 | 8 | _hyp_null_complete | \ex x (A \imp B) \imp \ex x A \imp \fo x A |
| 10 | 6, 9 | _hyp_mp | \ex x (A \imp B) \imp (\fo x A \imp \ex x B) \imp \ex x A \imp \ex x B |
| 11 | iff_eliml | (\ex x (A \imp B) \iff \fo x A \imp \ex x B) \imp \ex x (A \imp B) \imp \fo x A \imp \ex x B |
|
| 12 | 11 | _hyp_null_complete | \ex x (A \imp B) \imp (\ex x (A \imp B) \iff \fo x A \imp \ex x B) \imp \ex x (A \imp B) \imp \fo x A \imp \ex x B |
| 13 | ex_imp_distto_fo_ex | \ex x (A \imp B) \iff \fo x A \imp \ex x B |
|
| 14 | 13 | _hyp_null_complete | \ex x (A \imp B) \imp (\ex x (A \imp B) \iff \fo x A \imp \ex x B) |
| 15 | 12, 14 | _hyp_mp | \ex x (A \imp B) \imp \ex x (A \imp B) \imp \fo x A \imp \ex x B |
| 16 | _hyp_null_intro | \ex x (A \imp B) \imp \ex x (A \imp B) |
|
| 17 | 15, 16 | _hyp_mp | \ex x (A \imp B) \imp \fo x A \imp \ex x B |
| 18 | 10, 17 | _hyp_mp | \ex x (A \imp B) \imp \ex x A \imp \ex x B |
| 19 | 4, 18 | _hyp_mp | \ex x (A \imp B) \imp (\ex x B \imp \fo x B) \imp \ex x A \imp \fo x B |
| 20 | hyp h2 | \nf x B |
|
| 21 | 20 | conv nf | \ex x B \imp \fo x B |
| 22 | 21 | _hyp_null_complete | \ex x (A \imp B) \imp \ex x B \imp \fo x B |
| 23 | 19, 22 | _hyp_mp | \ex x (A \imp B) \imp \ex x A \imp \fo x B |
| 24 | 2, 23 | _hyp_mp | \ex x (A \imp B) \imp \fo x (A \imp B) |
| 25 | 24 | conv nf | \nf x (A \imp B) |