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 ⊢ 𝐴 ∈ V
frminex.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion frminex ( 𝑅 Fr 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 frminex.1 ⊢ 𝐴 ∈ V
2 frminex.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3 rabn0 ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
4 1 rabex ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V
5 ssrab2 ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
6 fri ⊢ ( ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) ) → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 )
7 2 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) )
8 7 rexbii ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) )
9 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝑥 ) )
10 9 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑦 𝑅 𝑧 ↔ ¬ 𝑦 𝑅 𝑥 ) )
11 10 imbi2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) ↔ ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
12 11 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
13 12 rexrab2 ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
14 8 13 bitri ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ¬ 𝑦 𝑅 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
15 6 14 sylib ⊢ ( ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
16 15 an4s ⊢ ( ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ) ∧ ( 𝑅 Fr 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
17 4 5 16 mpanl12 ⊢ ( ( 𝑅 Fr 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) )
18 17 ex ⊢ ( 𝑅 Fr 𝐴 → ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) ) )
19 3 18 biimtrrid ⊢ ( 𝑅 Fr 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → ¬ 𝑦 𝑅 𝑥 ) ) ) )