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

Metamath Proof Explorer

Theorem welb

Description: A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion welb ⊢ R We A ∧ B ∈ C ∧ B ⊆ A ∧ B ≠ ∅ → R -1 Or B ∧ ∃ x ∈ B ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ B y R -1 x → ∃ z ∈ B y R -1 z

Proof

Step Hyp Ref Expression
1 wess ⊢ B ⊆ A → R We A → R We B
2 1 impcom ⊢ R We A ∧ B ⊆ A → R We B
3 weso ⊢ R We B → R Or B
4 2 3 syl ⊢ R We A ∧ B ⊆ A → R Or B
5 cnvso ⊢ R Or B ↔ R -1 Or B
6 4 5 sylib ⊢ R We A ∧ B ⊆ A → R -1 Or B
7 6 3ad2antr2 ⊢ R We A ∧ B ∈ C ∧ B ⊆ A ∧ B ≠ ∅ → R -1 Or B
8 wefr ⊢ R We B → R Fr B
9 2 8 syl ⊢ R We A ∧ B ⊆ A → R Fr B
10 9 3ad2antr2 ⊢ R We A ∧ B ∈ C ∧ B ⊆ A ∧ B ≠ ∅ → R Fr B
11 ssidd ⊢ B ⊆ A → B ⊆ B
12 11 3anim2i ⊢ B ∈ C ∧ B ⊆ A ∧ B ≠ ∅ → B ∈ C ∧ B ⊆ B ∧ B ≠ ∅
13 12 adantl ⊢ R We A ∧ B ∈ C ∧ B ⊆ A ∧ B ≠ ∅ → B ∈ C ∧ B ⊆ B ∧ B ≠ ∅
14 frinfm ⊢ R Fr B ∧ B ∈ C ∧ B ⊆ B ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ B y R -1 x → ∃ z ∈ B y R -1 z
15 10 13 14 syl2anc ⊢ R We A ∧ B ∈ C ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ B y R -1 x → ∃ z ∈ B y R -1 z
16 7 15 jca ⊢ R We A ∧ B ∈ C ∧ B ⊆ A ∧ B ≠ ∅ → R -1 Or B ∧ ∃ x ∈ B ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ B y R -1 x → ∃ z ∈ B y R -1 z