Metamath Proof Explorer


Theorem sorpssint

Description: In a chain of sets, a minimal element is the intersection of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpssint
|- ( [C.] Or Y -> ( E. u e. Y A. v e. Y -. v C. u <-> |^| Y e. Y ) )

Proof

Step Hyp Ref Expression
1 intss1
 |-  ( u e. Y -> |^| Y C_ u )
2 1 3ad2ant2
 |-  ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> |^| Y C_ u )
3 sorpssi
 |-  ( ( [C.] Or Y /\ ( u e. Y /\ v e. Y ) ) -> ( u C_ v \/ v C_ u ) )
4 3 anassrs
 |-  ( ( ( [C.] Or Y /\ u e. Y ) /\ v e. Y ) -> ( u C_ v \/ v C_ u ) )
5 sspss
 |-  ( v C_ u <-> ( v C. u \/ v = u ) )
6 orel1
 |-  ( -. v C. u -> ( ( v C. u \/ v = u ) -> v = u ) )
7 eqimss2
 |-  ( v = u -> u C_ v )
8 6 7 syl6com
 |-  ( ( v C. u \/ v = u ) -> ( -. v C. u -> u C_ v ) )
9 5 8 sylbi
 |-  ( v C_ u -> ( -. v C. u -> u C_ v ) )
10 9 jao1i
 |-  ( ( u C_ v \/ v C_ u ) -> ( -. v C. u -> u C_ v ) )
11 4 10 syl
 |-  ( ( ( [C.] Or Y /\ u e. Y ) /\ v e. Y ) -> ( -. v C. u -> u C_ v ) )
12 11 ralimdva
 |-  ( ( [C.] Or Y /\ u e. Y ) -> ( A. v e. Y -. v C. u -> A. v e. Y u C_ v ) )
13 12 3impia
 |-  ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> A. v e. Y u C_ v )
14 ssint
 |-  ( u C_ |^| Y <-> A. v e. Y u C_ v )
15 13 14 sylibr
 |-  ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> u C_ |^| Y )
16 2 15 eqssd
 |-  ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> |^| Y = u )
17 simp2
 |-  ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> u e. Y )
18 16 17 eqeltrd
 |-  ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> |^| Y e. Y )
19 18 rexlimdv3a
 |-  ( [C.] Or Y -> ( E. u e. Y A. v e. Y -. v C. u -> |^| Y e. Y ) )
20 intss1
 |-  ( v e. Y -> |^| Y C_ v )
21 ssnpss
 |-  ( |^| Y C_ v -> -. v C. |^| Y )
22 20 21 syl
 |-  ( v e. Y -> -. v C. |^| Y )
23 22 rgen
 |-  A. v e. Y -. v C. |^| Y
24 psseq2
 |-  ( u = |^| Y -> ( v C. u <-> v C. |^| Y ) )
25 24 notbid
 |-  ( u = |^| Y -> ( -. v C. u <-> -. v C. |^| Y ) )
26 25 ralbidv
 |-  ( u = |^| Y -> ( A. v e. Y -. v C. u <-> A. v e. Y -. v C. |^| Y ) )
27 26 rspcev
 |-  ( ( |^| Y e. Y /\ A. v e. Y -. v C. |^| Y ) -> E. u e. Y A. v e. Y -. v C. u )
28 23 27 mpan2
 |-  ( |^| Y e. Y -> E. u e. Y A. v e. Y -. v C. u )
29 19 28 impbid1
 |-  ( [C.] Or Y -> ( E. u e. Y A. v e. Y -. v C. u <-> |^| Y e. Y ) )