wf_induction

Theorem wf_induction_set

Theorem. wf_induction_set
wf R M → A ⊆ M → (∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → y ∈ A) → x ∈ A) → A = M

Proof
01. 1 ⊢ A ⊆ M, hypo.
02. 2 ⊢ M \ A = ∅, hypo.
03. 2 ⊢ M ⊆ A, empty_diff 2.
04. 1, 2 ⊢ A = M, incl_antisym 1 3.
05. 1 ⊢ M \ A = ∅ → A = M, subj_intro 4.
06. 1 ⊢ ¬A = M → ¬M \ A = ∅, contraposition 5.
07. 7 ⊢ ¬A = M, hypo.
08. 1, 7 ⊢ ¬M \ A = ∅, subj_elim 6 7.
09. 9 ⊢ wf R M, hypo.
10. 9 ⊢ ∀A. A ⊆ M → ¬A = ∅ → ∃y. y ∈ A ∧ ¬∃x. x ∈ A ∧ (x, y) ∈ R,
  wf_unfold 9.
11. 9 ⊢ M \ A ⊆ M → ¬M \ A = ∅ → ∃y. y ∈ M \ A ∧ ¬∃x. x ∈ M \ A ∧ (x, y) ∈ R,
  uq_elim 10.
12. ⊢ M \ A ⊆ M, diff_incl.
13. 9 ⊢ ¬M \ A = ∅ → ∃y. y ∈ M \ A ∧ ¬∃x. x ∈ M \ A ∧ (x, y) ∈ R,
  subj_elim 11 12.
14. 9, 1, 7 ⊢ ∃y. y ∈ M \ A ∧ ¬∃x. x ∈ M \ A ∧ (x, y) ∈ R,
  subj_elim 13 8.
15. 15 ⊢ y ∈ M \ A ∧ ¬∃x. x ∈ M \ A ∧ (x, y) ∈ R, hypo.
16. 15 ⊢ y ∈ M \ A, conj_eliml 15.
17. 15 ⊢ y ∈ M, incl_elim 12 16.
18. 15 ⊢ ¬∃x. x ∈ M \ A ∧ (x, y) ∈ R, conj_elimr 15.
19. 15 ⊢ ∀x. x ∈ M \ A → ¬(x, y) ∈ R, neg_ex_bounded 18.
20. 15 ⊢ x ∈ M \ A → ¬(x, y) ∈ R, uq_elim 19.
21. 21 ⊢ ∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → y ∈ A) → x ∈ A, hypo.
22. 21 ⊢ y ∈ M → (∀x. x ∈ M → (x, y) ∈ R → x ∈ A) → y ∈ A, uq_elim 21.
23. 21, 15 ⊢ (∀x. x ∈ M → (x, y) ∈ R → x ∈ A) → y ∈ A, subj_elim 22 17.
24. 21, 15 ⊢ ¬y ∈ A → ¬(∀x. x ∈ M → (x, y) ∈ R → x ∈ A), contraposition 23.
25. 15 ⊢ ¬y ∈ A, diff_elimr 16.
26. 21, 15 ⊢ ¬(∀x. x ∈ M → (x, y) ∈ R → x ∈ A), subj_elim 24 25.
27. 21, 15 ⊢ ∃x. x ∈ M ∧ ¬((x, y) ∈ R → x ∈ A), neg_uq_bounded 26.
28. 28 ⊢ x ∈ M ∧ ¬((x, y) ∈ R → x ∈ A), hypo.
29. 28 ⊢ x ∈ M, conj_eliml 28.
30. 28 ⊢ ¬((x, y) ∈ R → x ∈ A), conj_elimr 28.
31. 28 ⊢ (x, y) ∈ R ∧ ¬x ∈ A, neg_subj 30.
32. 28 ⊢ (x, y) ∈ R, conj_eliml 31.
33. 28 ⊢ ¬x ∈ A, conj_elimr 31.
34. 28 ⊢ x ∈ M \ A, diff_intro 29 33.
35. 15, 28 ⊢ ¬(x, y) ∈ R, subj_elim 20 34.
36. 15, 28 ⊢ ⊥, neg_elim 35 32.
37. 21, 15 ⊢ ⊥, ex_elim 27 36.
38. 9, 1, 21, 7 ⊢ ⊥, ex_elim 14 37.
39. 9, 1, 21 ⊢ ¬¬A = M, neg_intro 38.
40. 9, 1, 21 ⊢ A = M, dne 39.
wf_induction_set. ⊢ wf R M → A ⊆ M →
  (∀x. x ∈ M → (∀y. y ∈ M → (y, x) ∈ R → y ∈ A) → x ∈ A) → A = M,
  subj_intro_iii 40.

Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, lem.