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 𝐴 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )