Metamath Proof Explorer

Theorem cutlt

Description: Eliminating all elements below a given element of a cut does not affect the cut. (Contributed by Scott Fenton, 13-Mar-2025)

Ref Expression
Hypotheses cutlt.1 
|- ( ph -> L <
cutlt.2 
|- ( ph -> A = ( L |s R ) )
cutlt.3 
|- ( ph -> X e. L )
Assertion cutlt 
|- ( ph -> A = ( ( { X } u. { y e. L | X

Proof

Step Hyp Ref Expression
1 cutlt.1 
 |-  ( ph -> L <
2 cutlt.2 
 |-  ( ph -> A = ( L |s R ) )
3 cutlt.3 
 |-  ( ph -> X e. L )
4 ssltss1 
 |-  ( L < L C_ No )
5 1 4 syl 
 |-  ( ph -> L C_ No )
6 5 3 sseldd 
 |-  ( ph -> X e. No )
7 snelpwi 
 |-  ( X e. No -> { X } e. ~P No )
8 6 7 syl 
 |-  ( ph -> { X } e. ~P No )
9 ssltex1 
 |-  ( L < L e. _V )
10 rabexg 
 |-  ( L e. _V -> { y e. L | X
11 1 9 10 3syl 
 |-  ( ph -> { y e. L | X
12 ssrab2 
 |-  { y e. L | X
13 12 5 sstrid 
 |-  ( ph -> { y e. L | X
14 11 13 elpwd 
 |-  ( ph -> { y e. L | X
15 pwuncl 
 |-  ( ( { X } e. ~P No /\ { y e. L | X  ( { X } u. { y e. L | X
16 8 14 15 syl2anc 
 |-  ( ph -> ( { X } u. { y e. L | X
17 ssltex2 
 |-  ( L < R e. _V )
18 1 17 syl 
 |-  ( ph -> R e. _V )
19 ssltss2 
 |-  ( L < R C_ No )
20 1 19 syl 
 |-  ( ph -> R C_ No )
21 18 20 elpwd 
 |-  ( ph -> R e. ~P No )
22 snidg 
 |-  ( X e. L -> X e. { X } )
23 elun1 
 |-  ( X e. { X } -> X e. ( { X } u. { y e. L | X
24 3 22 23 3syl 
 |-  ( ph -> X e. ( { X } u. { y e. L | X
25 24 adantr 
 |-  ( ( ph /\ a e. L ) -> X e. ( { X } u. { y e. L | X
26 breq2 
 |-  ( b = X -> ( a <_s b <-> a <_s X ) )
27 26 rspcev 
 |-  ( ( X e. ( { X } u. { y e. L | X  E. b e. ( { X } u. { y e. L | X
28 25 27 sylan 
 |-  ( ( ( ph /\ a e. L ) /\ a <_s X ) -> E. b e. ( { X } u. { y e. L | X
29 28 ex 
 |-  ( ( ph /\ a e. L ) -> ( a <_s X -> E. b e. ( { X } u. { y e. L | X
30 6 adantr 
 |-  ( ( ph /\ a e. L ) -> X e. No )
31 5 sselda 
 |-  ( ( ph /\ a e. L ) -> a e. No )
32 sltnle 
 |-  ( ( X e. No /\ a e. No ) -> ( X  -. a <_s X ) )
33 30 31 32 syl2anc 
 |-  ( ( ph /\ a e. L ) -> ( X  -. a <_s X ) )
34 breq2 
 |-  ( y = a -> ( X  X
35 34 elrab 
 |-  ( a e. { y e. L | X  ( a e. L /\ X
36 elun2 
 |-  ( a e. { y e. L | X  a e. ( { X } u. { y e. L | X
37 35 36 sylbir 
 |-  ( ( a e. L /\ X  a e. ( { X } u. { y e. L | X
38 slerflex 
 |-  ( a e. No -> a <_s a )
39 31 38 syl 
 |-  ( ( ph /\ a e. L ) -> a <_s a )
40 39 adantrr 
 |-  ( ( ph /\ ( a e. L /\ X  a <_s a )
41 breq2 
 |-  ( b = a -> ( a <_s b <-> a <_s a ) )
42 41 rspcev 
 |-  ( ( a e. ( { X } u. { y e. L | X  E. b e. ( { X } u. { y e. L | X
43 37 40 42 syl2an2 
 |-  ( ( ph /\ ( a e. L /\ X  E. b e. ( { X } u. { y e. L | X
44 43 expr 
 |-  ( ( ph /\ a e. L ) -> ( X  E. b e. ( { X } u. { y e. L | X
45 33 44 sylbird 
 |-  ( ( ph /\ a e. L ) -> ( -. a <_s X -> E. b e. ( { X } u. { y e. L | X
46 29 45 pm2.61d 
 |-  ( ( ph /\ a e. L ) -> E. b e. ( { X } u. { y e. L | X
47 46 ralrimiva 
 |-  ( ph -> A. a e. L E. b e. ( { X } u. { y e. L | X
48 ssidd 
 |-  ( ph -> R C_ R )
49 20 48 coiniss 
 |-  ( ph -> A. a e. R E. b e. R b <_s a )
50 3 snssd 
 |-  ( ph -> { X } C_ L )
51 12 a1i 
 |-  ( ph -> { y e. L | X
52 50 51 unssd 
 |-  ( ph -> ( { X } u. { y e. L | X
53 5 52 cofss 
 |-  ( ph -> A. a e. ( { X } u. { y e. L | X
54 1 16 21 47 49 53 49 cofcut2d 
 |-  ( ph -> ( L |s R ) = ( ( { X } u. { y e. L | X
55 2 54 eqtrd 
 |-  ( ph -> A = ( ( { X } u. { y e. L | X