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

Metamath Proof Explorer

Theorem frminex

Description: If an element of a well-founded set satisfies a property ph , then there is a minimal element that satisfies ph . (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 18-Nov-2016)

Ref Expression
Hypotheses frminex.1 ⊢ A ∈ V
frminex.2 ⊢ x = y → φ ↔ ψ
Assertion frminex ⊢ R Fr A → ∃ x ∈ A φ → ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x

Proof

Step Hyp Ref Expression
1 frminex.1 ⊢ A ∈ V
2 frminex.2 ⊢ x = y → φ ↔ ψ
3 rabn0 ⊢ x ∈ A | φ ≠ ∅ ↔ ∃ x ∈ A φ
4 1 rabex ⊢ x ∈ A | φ ∈ V
5 ssrab2 ⊢ x ∈ A | φ ⊆ A
6 fri ⊢ x ∈ A | φ ∈ V ∧ R Fr A ∧ x ∈ A | φ ⊆ A ∧ x ∈ A | φ ≠ ∅ → ∃ z ∈ x ∈ A | φ ∀ y ∈ x ∈ A | φ ¬ y R z
7 2 ralrab ⊢ ∀ y ∈ x ∈ A | φ ¬ y R z ↔ ∀ y ∈ A ψ → ¬ y R z
8 7 rexbii ⊢ ∃ z ∈ x ∈ A | φ ∀ y ∈ x ∈ A | φ ¬ y R z ↔ ∃ z ∈ x ∈ A | φ ∀ y ∈ A ψ → ¬ y R z
9 breq2 ⊢ z = x → y R z ↔ y R x
10 9 notbid ⊢ z = x → ¬ y R z ↔ ¬ y R x
11 10 imbi2d ⊢ z = x → ψ → ¬ y R z ↔ ψ → ¬ y R x
12 11 ralbidv ⊢ z = x → ∀ y ∈ A ψ → ¬ y R z ↔ ∀ y ∈ A ψ → ¬ y R x
13 12 rexrab2 ⊢ ∃ z ∈ x ∈ A | φ ∀ y ∈ A ψ → ¬ y R z ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x
14 8 13 bitri ⊢ ∃ z ∈ x ∈ A | φ ∀ y ∈ x ∈ A | φ ¬ y R z ↔ ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x
15 6 14 sylib ⊢ x ∈ A | φ ∈ V ∧ R Fr A ∧ x ∈ A | φ ⊆ A ∧ x ∈ A | φ ≠ ∅ → ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x
16 15 an4s ⊢ x ∈ A | φ ∈ V ∧ x ∈ A | φ ⊆ A ∧ R Fr A ∧ x ∈ A | φ ≠ ∅ → ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x
17 4 5 16 mpanl12 ⊢ R Fr A ∧ x ∈ A | φ ≠ ∅ → ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x
18 17 ex ⊢ R Fr A → x ∈ A | φ ≠ ∅ → ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x
19 3 18 biimtrrid ⊢ R Fr A → ∃ x ∈ A φ → ∃ x ∈ A φ ∧ ∀ y ∈ A ψ → ¬ y R x