Metamath Proof Explorer

Theorem frinfm

Description: A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion frinfm 
|- ( ( R Fr A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )

Proof

Step Hyp Ref Expression
1 fri 
 |-  ( ( ( B e. C /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
2 1 ancom1s 
 |-  ( ( ( R Fr A /\ B e. C ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
3 2 exp43 
 |-  ( R Fr A -> ( B e. C -> ( B C_ A -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) ) ) )
4 3 3imp2 
 |-  ( ( R Fr A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
5 ssel2 
 |-  ( ( B C_ A /\ x e. B ) -> x e. A )
6 5 adantrr 
 |-  ( ( B C_ A /\ ( x e. B /\ A. y e. B -. y R x ) ) -> x e. A )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 brcnv 
 |-  ( x `' R y <-> y R x )
10 9 biimpi 
 |-  ( x `' R y -> y R x )
11 10 con3i 
 |-  ( -. y R x -> -. x `' R y )
12 11 ralimi 
 |-  ( A. y e. B -. y R x -> A. y e. B -. x `' R y )
13 12 ad2antll 
 |-  ( ( B C_ A /\ ( x e. B /\ A. y e. B -. y R x ) ) -> A. y e. B -. x `' R y )
14 breq2 
 |-  ( z = x -> ( y `' R z <-> y `' R x ) )
15 14 rspcev 
 |-  ( ( x e. B /\ y `' R x ) -> E. z e. B y `' R z )
16 15 ex 
 |-  ( x e. B -> ( y `' R x -> E. z e. B y `' R z ) )
17 16 ralrimivw 
 |-  ( x e. B -> A. y e. A ( y `' R x -> E. z e. B y `' R z ) )
18 17 ad2antrl 
 |-  ( ( B C_ A /\ ( x e. B /\ A. y e. B -. y R x ) ) -> A. y e. A ( y `' R x -> E. z e. B y `' R z ) )
19 6 13 18 jca32 
 |-  ( ( B C_ A /\ ( x e. B /\ A. y e. B -. y R x ) ) -> ( x e. A /\ ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) )
20 19 ex 
 |-  ( B C_ A -> ( ( x e. B /\ A. y e. B -. y R x ) -> ( x e. A /\ ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) ) )
21 20 reximdv2 
 |-  ( B C_ A -> ( E. x e. B A. y e. B -. y R x -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) )
22 21 adantl 
 |-  ( ( R Fr A /\ B C_ A ) -> ( E. x e. B A. y e. B -. y R x -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) )
23 22 3ad2antr2 
 |-  ( ( R Fr A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> ( E. x e. B A. y e. B -. y R x -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) )
24 4 23 mpd 
 |-  ( ( R Fr A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )