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 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
weinfcl.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
weinfcl.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
weinfcl.4 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
Assertion weinfcl ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 weinfcl.1 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
2 weinfcl.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3 weinfcl.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
4 weinfcl.4 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
5 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
6 1 5 syl ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
7 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) → 𝑅 Or 𝐴 )
8 3 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝑖 ∈ 𝐴 )
9 8 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) → 𝑖 ∈ 𝐴 )
10 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑖 ↔ 𝑦 𝑅 𝑖 ) )
11 10 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 𝑅 𝑖 ↔ ¬ 𝑦 𝑅 𝑖 ) )
12 11 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑖 )
13 12 bilani ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) → ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑖 )
14 13 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝑦 𝑅 𝑖 )
15 breq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 𝑅 𝑦 ↔ 𝑖 𝑅 𝑦 ) )
16 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑖 𝑅 𝑦 ) ) → 𝑖 ∈ 𝐵 )
17 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑖 𝑅 𝑦 ) ) → 𝑖 𝑅 𝑦 )
18 15 16 17 rspcedvdw ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑖 𝑅 𝑦 ) ) → ∃ 𝑗 ∈ 𝐵 𝑗 𝑅 𝑦 )
19 7 9 14 18 eqinfd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝑖 )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) → 𝑖 ∈ 𝐵 )
21 19 20 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 ) → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )
22 wefr ⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
23 1 22 syl ⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
24 23 3 2 4 frd ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 𝑅 𝑖 )
25 21 24 r19.29a ⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )