Proof
01. 1 ⊢ wf R M, hypo.
02. 2 ⊢ A = {x | x ∈ M ∧ P x}, hypo.
03. 3 ⊢ ∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → P y) → P x, hypo.
04. 3 ⊢ x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → P y) → P x, uq_elim 3.
05. 5 ⊢ x ∈ M, hypo.
06. 3, 5 ⊢ (∀y. y ∈ M → (y, x) ∈ R → P y) → P x, subj_elim 4 5.
07. 7 ⊢ ∀y. y ∈ M → (y, x) ∈ R → y ∈ A, hypo.
08. 7 ⊢ y ∈ M → (y, x) ∈ R → y ∈ A, uq_elim 7.
09. 9 ⊢ y ∈ M, hypo.
10. 7, 9 ⊢ (y, x) ∈ R → y ∈ A, subj_elim 8 9.
11. 11 ⊢ (y, x) ∈ R, hypo.
12. 7, 9, 11 ⊢ y ∈ A, subj_elim 10 11.
13. 2, 7, 9, 11 ⊢ y ∈ {x | x ∈ M ∧ P x}, eq_subst 2 12, P u ↔ y ∈ u.
14. 2, 7, 9, 11 ⊢ y ∈ M ∧ P y, comp_elim 13.
15. 2, 7, 9, 11 ⊢ P y, conj_elimr 14.
16. 2, 7, 9 ⊢ (y, x) ∈ R → P y, subj_intro 15.
17. 2, 7 ⊢ y ∈ M → (y, x) ∈ R → P y, subj_intro 16.
18. 2, 7 ⊢ ∀y. y ∈ M → (y, x) ∈ R → P y, uq_intro 17.
19. 2, 3, 5, 7 ⊢ P x, subj_elim 6 18.
20. 2, 3, 5, 7 ⊢ x ∈ M ∧ P x, conj_intro 5 19.
21. 5 ⊢ set x, set_intro 5.
22. 2, 3, 5, 7 ⊢ x ∈ {x | x ∈ M ∧ P x}, comp_intro 21 20.
23. 2, 3, 5, 7 ⊢ x ∈ A, eq_subst_rev 2 22, P u ↔ x ∈ u.
24. 2, 3, 5 ⊢ (∀y. y ∈ M → (y, x) ∈ R → y ∈ A) → x ∈ A, subj_intro 23.
25. 2, 3 ⊢ x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → y ∈ A) → x ∈ A, subj_intro 24.
26. 2, 3 ⊢ ∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → y ∈ A) → x ∈ A, uq_intro 25.
27. 27 ⊢ x ∈ A, hypo.
28. 2, 27 ⊢ x ∈ {x | x ∈ M ∧ P x}, eq_subst 2 27, P u ↔ x ∈ u.
29. 2, 27 ⊢ x ∈ M ∧ P x, comp_elim 28.
30. 2, 27 ⊢ x ∈ M, conj_eliml 29.
31. 2 ⊢ x ∈ A → x ∈ M, subj_intro 30.
32. 2 ⊢ ∀x. x ∈ A → x ∈ M, uq_intro 31.
33. 2 ⊢ A ⊆ M, incl_intro 32.
34. 1, 2, 3 ⊢ A = M, wf_induction_set 1 33 26.
35. 35 ⊢ x ∈ M, hypo.
36. 1, 2, 3, 35 ⊢ x ∈ A, eq_subst_rev 34 35, P u ↔ x ∈ u.
37. 1, 2, 3, 35 ⊢ x ∈ {x | x ∈ M ∧ P x}, eq_subst 2 36, P u ↔ x ∈ u.
38. 1, 2, 3, 35 ⊢ x ∈ M ∧ P x, comp_elim 37.
39. 1, 2, 3, 35 ⊢ P x, conj_elimr 38.
40. 1, 2, 3 ⊢ x ∈ M → P x, subj_intro 39.
41. 1, 3, 2 ⊢ ∀x. x ∈ M → P x, uq_intro 40.
42. 1, 3 ⊢ A = {x | x ∈ M ∧ P x} → ∀x. x ∈ M → P x, subj_intro 41.
43. 1, 3 ⊢ {x | x ∈ M ∧ P x} = {x | x ∈ M ∧ P x} → ∀x. x ∈ M → P x, 42.
44. ⊢ {x | x ∈ M ∧ P x} = {x | x ∈ M ∧ P x}, eq_refl.
45. 1, 3 ⊢ ∀x. x ∈ M → P x, subj_elim 43 44.
wf_induction. ⊢ wf R M →
(∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → P y) → P x) →
(∀x. x ∈ M → P x), subj_intro_ii 45.
Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, lem.