Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frinfm Structured version   Unicode version

Theorem frinfm 26439
 Description: A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
frinfm
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem frinfm
StepHypRef Expression
1 fri 4546 . . . . 5
21ancom1s 782 . . . 4
32exp43 597 . . 3
433imp2 1169 . 2
5 ssel2 3345 . . . . . . . 8
65adantrr 699 . . . . . . 7
7 vex 2961 . . . . . . . . . . . 12
8 vex 2961 . . . . . . . . . . . 12
97, 8brcnv 5057 . . . . . . . . . . 11
109biimpi 188 . . . . . . . . . 10
1110con3i 130 . . . . . . . . 9
1211ralimi 2783 . . . . . . . 8
1312ad2antll 711 . . . . . . 7
14 breq2 4218 . . . . . . . . . . 11
1514rspcev 3054 . . . . . . . . . 10
1615ex 425 . . . . . . . . 9
1716ralrimivw 2792 . . . . . . . 8
1817ad2antrl 710 . . . . . . 7
196, 13, 18jca32 523 . . . . . 6
2019ex 425 . . . . 5
2120reximdv2 2817 . . . 4