Theorem fisup2g

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

	Ref	Expression
Assertion	fisup2g	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		soss	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → 𝑅 Or 𝐵 ) )
2		simp1	⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → 𝑅 Or 𝐵 )
3		fisupg	⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
4	2 3	supeu	⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
5	4	3exp	⊢ ( 𝑅 Or 𝐵 → ( 𝐵 ∈ Fin → ( 𝐵 ≠ ∅ → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) )
6	1 5	syl6	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → ( 𝐵 ∈ Fin → ( 𝐵 ≠ ∅ → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) ) )
7	6	com4l	⊢ ( 𝑅 Or 𝐴 → ( 𝐵 ∈ Fin → ( 𝐵 ≠ ∅ → ( 𝐵 ⊆ 𝐴 → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) ) )
8	7	3imp2	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
9		reurex	⊢ ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
10		breq2	⊢ ( 𝑧 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝑥 ) )
11	10	rspcev	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 )
12	11	ex	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
13	12	ralrimivw	⊢ ( 𝑥 ∈ 𝐵 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
14	13	a1d	⊢ ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
15	14	anim2d	⊢ ( 𝑥 ∈ 𝐵 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) )
16	15	reximia	⊢ ( ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
17	8 9 16	3syl	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )