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 
|- ( ph -> R We A )
weinfcl.2 
|- ( ph -> B e. V )
weinfcl.3 
|- ( ph -> B C_ A )
weinfcl.4 
|- ( ph -> B =/= (/) )
Assertion weinfcl 
|- ( ph -> inf ( B , A , R ) e. B )

Proof

Step Hyp Ref Expression
1 weinfcl.1 
 |-  ( ph -> R We A )
2 weinfcl.2 
 |-  ( ph -> B e. V )
3 weinfcl.3 
 |-  ( ph -> B C_ A )
4 weinfcl.4 
 |-  ( ph -> B =/= (/) )
5 weso 
 |-  ( R We A -> R Or A )
6 1 5 syl 
 |-  ( ph -> R Or A )
7 6 ad2antrr 
 |-  ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) -> R Or A )
8 3 sselda 
 |-  ( ( ph /\ i e. B ) -> i e. A )
9 8 adantr 
 |-  ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) -> i e. 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 
 |-  ( A. x e. B -. x R i <-> A. y e. B -. y R i )
13 12 bilani 
 |-  ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) -> A. y e. B -. y R i )
14 13 r19.21bi 
 |-  ( ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) /\ y e. B ) -> -. y R i )
15 breq1 
 |-  ( j = i -> ( j R y <-> i R y ) )
16 simpllr 
 |-  ( ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) /\ ( y e. A /\ i R y ) ) -> i e. B )
17 simprr 
 |-  ( ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) /\ ( y e. A /\ i R y ) ) -> i R y )
18 15 16 17 rspcedvdw 
 |-  ( ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) /\ ( y e. A /\ i R y ) ) -> E. j e. B j R y )
19 7 9 14 18 eqinfd 
 |-  ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) -> inf ( B , A , R ) = i )
20 simplr 
 |-  ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) -> i e. B )
21 19 20 eqeltrd 
 |-  ( ( ( ph /\ i e. B ) /\ A. x e. B -. x R i ) -> inf ( B , A , R ) e. B )
22 wefr 
 |-  ( R We A -> R Fr A )
23 1 22 syl 
 |-  ( ph -> R Fr A )
24 23 3 2 4 frd 
 |-  ( ph -> E. i e. B A. x e. B -. x R i )
25 21 24 r19.29a 
 |-  ( ph -> inf ( B , A , R ) e. B )