Metamath Proof Explorer

Theorem weinfcl

Description: Closure of the infimum in a well-order. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses weinfcl.1 ⊢ φ → R We A
weinfcl.2 ⊢ φ → B ∈ V
weinfcl.3 ⊢ φ → B ⊆ A
weinfcl.4 ⊢ φ → B ≠ ∅
Assertion weinfcl ⊢ φ → inf B A R ∈ B

Proof

Step Hyp Ref Expression
1 weinfcl.1 ⊢ φ → R We A
2 weinfcl.2 ⊢ φ → B ∈ V
3 weinfcl.3 ⊢ φ → B ⊆ A
4 weinfcl.4 ⊢ φ → B ≠ ∅
5 weso ⊢ R We A → R Or A
6 1 5 syl ⊢ φ → R Or A
7 6 ad2antrr ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i → R Or A
8 3 sselda ⊢ φ ∧ i ∈ B → i ∈ A
9 8 adantr ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i → i ∈ A
10 breq1 ⊢ x = y → x R i ↔ y R i
11 10 notbid ⊢ x = y → ¬ x R i ↔ ¬ y R i
12 11 cbvralvw ⊢ ∀ x ∈ B ¬ x R i ↔ ∀ y ∈ B ¬ y R i
13 12 bilani ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i → ∀ y ∈ B ¬ y R i
14 13 r19.21bi ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i ∧ y ∈ B → ¬ y R i
15 breq1 ⊢ j = i → j R y ↔ i R y
16 simpllr ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i ∧ y ∈ A ∧ i R y → i ∈ B
17 simprr ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i ∧ y ∈ A ∧ i R y → i R y
18 15 16 17 rspcedvdw ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i ∧ y ∈ A ∧ i R y → ∃ j ∈ B j R y
19 7 9 14 18 eqinfd ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i → inf B A R = i
20 simplr ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i → i ∈ B
21 19 20 eqeltrd ⊢ φ ∧ i ∈ B ∧ ∀ x ∈ B ¬ x R i → inf B A R ∈ B
22 wefr ⊢ R We A → R Fr A
23 1 22 syl ⊢ φ → R Fr A
24 23 3 2 4 frd ⊢ φ → ∃ i ∈ B ∀ x ∈ B ¬ x R i
25 21 24 r19.29a ⊢ φ → inf B A R ∈ B