This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frd

Description: A nonempty subset of an R -well-founded class has an R -minimal element (deduction form). (Contributed by BJ, 16-Nov-2024)

Ref Expression
Hypotheses frd.fr ⊢ φ → R Fr A
frd.ss ⊢ φ → B ⊆ A
frd.ex ⊢ φ → B ∈ V
frd.n0 ⊢ φ → B ≠ ∅
Assertion frd ⊢ φ → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 frd.fr ⊢ φ → R Fr A
2 frd.ss ⊢ φ → B ⊆ A
3 frd.ex ⊢ φ → B ∈ V
4 frd.n0 ⊢ φ → B ≠ ∅
5 simpr ⊢ φ ∧ z = B → z = B
6 biidd ⊢ φ ∧ z = B → ¬ y R x ↔ ¬ y R x
7 5 6 raleqbidv ⊢ φ ∧ z = B → ∀ y ∈ z ¬ y R x ↔ ∀ y ∈ B ¬ y R x
8 5 7 rexeqbidv ⊢ φ ∧ z = B → ∃ x ∈ z ∀ y ∈ z ¬ y R x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y R x
9 3 2 elpwd ⊢ φ → B ∈ 𝒫 A
10 nelsn ⊢ B ≠ ∅ → ¬ B ∈ ∅
11 4 10 syl ⊢ φ → ¬ B ∈ ∅
12 9 11 eldifd ⊢ φ → B ∈ 𝒫 A ∖ ∅
13 dffr6 ⊢ R Fr A ↔ ∀ z ∈ 𝒫 A ∖ ∅ ∃ x ∈ z ∀ y ∈ z ¬ y R x
14 1 13 sylib ⊢ φ → ∀ z ∈ 𝒫 A ∖ ∅ ∃ x ∈ z ∀ y ∈ z ¬ y R x
15 8 12 14 rspcdv2 ⊢ φ → ∃ x ∈ B ∀ y ∈ B ¬ y R x