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 ⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
frd.ss ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
frd.ex ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
frd.n0 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
Assertion frd ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 frd.fr ⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
2 frd.ss ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3 frd.ex ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4 frd.n0 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
6 biidd ⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑥 ) )
7 5 6 raleqbidv ⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
8 5 7 rexeqbidv ⊢ ( ( 𝜑 ∧ 𝑧 = 𝐵 ) → ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
9 3 2 elpwd ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐴 )
10 nelsn ⊢ ( 𝐵 ≠ ∅ → ¬ 𝐵 ∈ { ∅ } )
11 4 10 syl ⊢ ( 𝜑 → ¬ 𝐵 ∈ { ∅ } )
12 9 11 eldifd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
13 dffr6 ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 )
14 1 13 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 )
15 8 12 14 rspcdv2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )