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 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )