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 ) )