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

Metamath Proof Explorer

Theorem wereu

Description: A nonempty subset of an R -well-ordered class has a unique R -minimal element. (Contributed by NM, 18-Mar-1997) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion wereu ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 wefr ⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
2 fri ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑅 Fr 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
3 2 exp32 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑅 Fr 𝐴 ) → ( 𝐵 ⊆ 𝐴 → ( 𝐵 ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
4 3 expcom ⊢ ( 𝑅 Fr 𝐴 → ( 𝐵 ∈ 𝑉 → ( 𝐵 ⊆ 𝐴 → ( 𝐵 ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) ) )
5 4 3imp2 ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
6 1 5 sylan ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
7 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
8 soss ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → 𝑅 Or 𝐵 ) )
9 7 8 mpan9 ⊢ ( ( 𝑅 We 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝑅 Or 𝐵 )
10 somo ⊢ ( 𝑅 Or 𝐵 → ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
11 9 10 syl ⊢ ( ( 𝑅 We 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
12 11 3ad2antr2 ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
13 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∃* 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
14 6 12 13 sylanbrc ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )