Metamath Proof Explorer

Theorem fisup2g

Description: A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion 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

Proof

Step Hyp Ref Expression
1 soss ⊢ B ⊆ A → R Or A → R Or B
2 simp1 ⊢ R Or B ∧ B ∈ Fin ∧ B ≠ ∅ → R Or B
3 fisupg ⊢ R Or B ∧ B ∈ Fin ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z
4 2 3 supeu ⊢ R Or B ∧ B ∈ Fin ∧ B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z
5 4 3exp ⊢ R Or B → B ∈ Fin → B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z
6 1 5 syl6 ⊢ B ⊆ A → R Or A → B ∈ Fin → B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ B y R z
7 6 com4l ⊢ 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
8 7 3imp2 ⊢ 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
9 reurex ⊢ ∃! 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
10 breq2 ⊢ z = x → y R z ↔ y R x
11 10 rspcev ⊢ x ∈ B ∧ y R x → ∃ z ∈ B y R z
12 11 ex ⊢ x ∈ B → y R x → ∃ z ∈ B y R z
13 12 ralrimivw ⊢ x ∈ B → ∀ y ∈ A y R x → ∃ z ∈ B y R z
14 13 a1d ⊢ x ∈ B → ∀ y ∈ B y R x → ∃ z ∈ B y R z → ∀ y ∈ A y R x → ∃ z ∈ B y R z
15 14 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
16 15 reximia ⊢ ∃ 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 ∈ A y R x → ∃ z ∈ B y R z
17 8 9 16 3syl ⊢ 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