This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fiinf2g

Description: A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 soss ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → 𝑅 Or 𝐵 ) )
2 simp1 ⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → 𝑅 Or 𝐵 )
3 fiinfg ⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
4 2 3 infeu ⊢ ( ( 𝑅 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 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝑅 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
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 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )