Metamath Proof Explorer

Theorem fin2solem

Description: Lemma for fin2so . (Contributed by Brendan Leahy, 29-Jun-2019)

Ref Expression
Assertion fin2solem 
|- ( ( R Or x /\ ( y e. x /\ z e. x ) ) -> ( y R z -> { w e. x | w R y } [C.] { w e. x | w R z } ) )

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( ( y e. x /\ z e. x ) /\ w e. x ) <-> ( w e. x /\ ( y e. x /\ z e. x ) ) )
2 3anass 
 |-  ( ( w e. x /\ y e. x /\ z e. x ) <-> ( w e. x /\ ( y e. x /\ z e. x ) ) )
3 1 2 bitr4i 
 |-  ( ( ( y e. x /\ z e. x ) /\ w e. x ) <-> ( w e. x /\ y e. x /\ z e. x ) )
4 sotr 
 |-  ( ( R Or x /\ ( w e. x /\ y e. x /\ z e. x ) ) -> ( ( w R y /\ y R z ) -> w R z ) )
5 3 4 sylan2b 
 |-  ( ( R Or x /\ ( ( y e. x /\ z e. x ) /\ w e. x ) ) -> ( ( w R y /\ y R z ) -> w R z ) )
6 5 anassrs 
 |-  ( ( ( R Or x /\ ( y e. x /\ z e. x ) ) /\ w e. x ) -> ( ( w R y /\ y R z ) -> w R z ) )
7 6 ancomsd 
 |-  ( ( ( R Or x /\ ( y e. x /\ z e. x ) ) /\ w e. x ) -> ( ( y R z /\ w R y ) -> w R z ) )
8 7 expdimp 
 |-  ( ( ( ( R Or x /\ ( y e. x /\ z e. x ) ) /\ w e. x ) /\ y R z ) -> ( w R y -> w R z ) )
9 8 an32s 
 |-  ( ( ( ( R Or x /\ ( y e. x /\ z e. x ) ) /\ y R z ) /\ w e. x ) -> ( w R y -> w R z ) )
10 9 ss2rabdv 
 |-  ( ( ( R Or x /\ ( y e. x /\ z e. x ) ) /\ y R z ) -> { w e. x | w R y } C_ { w e. x | w R z } )
11 breq1 
 |-  ( w = y -> ( w R z <-> y R z ) )
12 11 elrab 
 |-  ( y e. { w e. x | w R z } <-> ( y e. x /\ y R z ) )
13 12 biimpri 
 |-  ( ( y e. x /\ y R z ) -> y e. { w e. x | w R z } )
14 13 adantll 
 |-  ( ( ( R Or x /\ y e. x ) /\ y R z ) -> y e. { w e. x | w R z } )
15 sonr 
 |-  ( ( R Or x /\ y e. x ) -> -. y R y )
16 breq1 
 |-  ( w = y -> ( w R y <-> y R y ) )
17 16 elrab 
 |-  ( y e. { w e. x | w R y } <-> ( y e. x /\ y R y ) )
18 17 simprbi 
 |-  ( y e. { w e. x | w R y } -> y R y )
19 15 18 nsyl 
 |-  ( ( R Or x /\ y e. x ) -> -. y e. { w e. x | w R y } )
20 19 adantr 
 |-  ( ( ( R Or x /\ y e. x ) /\ y R z ) -> -. y e. { w e. x | w R y } )
21 nelne1 
 |-  ( ( y e. { w e. x | w R z } /\ -. y e. { w e. x | w R y } ) -> { w e. x | w R z } =/= { w e. x | w R y } )
22 21 necomd 
 |-  ( ( y e. { w e. x | w R z } /\ -. y e. { w e. x | w R y } ) -> { w e. x | w R y } =/= { w e. x | w R z } )
23 14 20 22 syl2anc 
 |-  ( ( ( R Or x /\ y e. x ) /\ y R z ) -> { w e. x | w R y } =/= { w e. x | w R z } )
24 23 adantlrr 
 |-  ( ( ( R Or x /\ ( y e. x /\ z e. x ) ) /\ y R z ) -> { w e. x | w R y } =/= { w e. x | w R z } )
25 vex 
 |-  x e. _V
26 25 rabex 
 |-  { w e. x | w R z } e. _V
27 26 brrpss 
 |-  ( { w e. x | w R y } [C.] { w e. x | w R z } <-> { w e. x | w R y } C. { w e. x | w R z } )
28 df-pss 
 |-  ( { w e. x | w R y } C. { w e. x | w R z } <-> ( { w e. x | w R y } C_ { w e. x | w R z } /\ { w e. x | w R y } =/= { w e. x | w R z } ) )
29 27 28 bitri 
 |-  ( { w e. x | w R y } [C.] { w e. x | w R z } <-> ( { w e. x | w R y } C_ { w e. x | w R z } /\ { w e. x | w R y } =/= { w e. x | w R z } ) )
30 10 24 29 sylanbrc 
 |-  ( ( ( R Or x /\ ( y e. x /\ z e. x ) ) /\ y R z ) -> { w e. x | w R y } [C.] { w e. x | w R z } )
31 30 ex 
 |-  ( ( R Or x /\ ( y e. x /\ z e. x ) ) -> ( y R z -> { w e. x | w R y } [C.] { w e. x | w R z } ) )