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 ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ( ◡ 𝑅 Or 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 wess ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 We 𝐴 → 𝑅 We 𝐵 ) )
2 1 impcom ⊢ ( ( 𝑅 We 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝑅 We 𝐵 )
3 weso ⊢ ( 𝑅 We 𝐵 → 𝑅 Or 𝐵 )
4 2 3 syl ⊢ ( ( 𝑅 We 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝑅 Or 𝐵 )
5 cnvso ⊢ ( 𝑅 Or 𝐵 ↔ ◡ 𝑅 Or 𝐵 )
6 4 5 sylib ⊢ ( ( 𝑅 We 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ◡ 𝑅 Or 𝐵 )
7 6 3ad2antr2 ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ◡ 𝑅 Or 𝐵 )
8 wefr ⊢ ( 𝑅 We 𝐵 → 𝑅 Fr 𝐵 )
9 2 8 syl ⊢ ( ( 𝑅 We 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝑅 Fr 𝐵 )
10 9 3ad2antr2 ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → 𝑅 Fr 𝐵 )
11 ssidd ⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 ⊆ 𝐵 )
12 11 3anim2i ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐵 ∧ 𝐵 ≠ ∅ ) )
13 12 adantl ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐵 ∧ 𝐵 ≠ ∅ ) )
14 frinfm ⊢ ( ( 𝑅 Fr 𝐵 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐵 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
15 10 13 14 syl2anc ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
16 7 15 jca ⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ( ◡ 𝑅 Or 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )