Metamath Proof Explorer

Theorem sorpssuni

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

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

Proof

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