Metamath Proof Explorer

Theorem fisupcl

Description: A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011)

Ref Expression
Assertion fisupcl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → sup B A R ∈ B

Proof

Step Hyp Ref Expression
1 simpl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → R Or A
2 1 supval2 ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
3 simpr3 ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → B ⊆ A
4 breq2 ⊢ z = x → y R z ↔ y R x
5 4 rspcev ⊢ x ∈ B ∧ y R x → ∃ z ∈ B y R z
6 5 ex ⊢ x ∈ B → y R x → ∃ z ∈ B y R z
7 6 ralrimivw ⊢ x ∈ B → ∀ y ∈ A y R x → ∃ z ∈ B y R z
8 7 a1d ⊢ x ∈ B → ∀ y ∈ B y R x → ∃ z ∈ B y R z → ∀ y ∈ A y R x → ∃ z ∈ B y R z
9 8 anim2d ⊢ x ∈ B → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
10 9 rgen ⊢ ∀ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
11 10 a1i ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∀ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
12 soss ⊢ B ⊆ A → R Or A → R Or B
13 3 1 12 sylc ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → R Or B
14 simpr1 ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → B ∈ Fin
15 simpr2 ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → B ≠ ∅
16 fisupg ⊢ R Or B ∧ B ∈ Fin ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z
17 13 14 15 16 syl3anc ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z
18 fisup2g ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
19 ssrexv ⊢ B ⊆ A → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
20 3 18 19 sylc ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
21 1 20 supeu ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
22 riotass2 ⊢ B ⊆ A ∧ ∀ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∧ ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z ∧ ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ι x ∈ B | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
23 3 11 17 21 22 syl22anc ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ι x ∈ B | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
24 13 17 supeu ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃! x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z
25 riotacl ⊢ ∃! x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z → ι x ∈ B | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z ∈ B
26 24 25 syl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ι x ∈ B | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z ∈ B
27 23 26 eqeltrrd ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∈ B
28 2 27 eqeltrd ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → sup B A R ∈ B