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