Metamath Proof Explorer

Theorem ordthauslem

Description: Lemma for ordthaus . (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis ordthauslem.1 
|- X = dom R
Assertion ordthauslem 
|- ( ( R e. TosetRel /\ A e. X /\ B e. X ) -> ( A R B -> ( A =/= B -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 ordthauslem.1 
 |-  X = dom R
2 simpll1 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> R e. TosetRel )
3 simpll3 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> B e. X )
4 1 ordtopn2 
 |-  ( ( R e. TosetRel /\ B e. X ) -> { x e. X | -. B R x } e. ( ordTop ` R ) )
5 2 3 4 syl2anc 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> { x e. X | -. B R x } e. ( ordTop ` R ) )
6 simpll2 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> A e. X )
7 1 ordtopn1 
 |-  ( ( R e. TosetRel /\ A e. X ) -> { x e. X | -. x R A } e. ( ordTop ` R ) )
8 2 6 7 syl2anc 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> { x e. X | -. x R A } e. ( ordTop ` R ) )
9 breq2 
 |-  ( x = A -> ( B R x <-> B R A ) )
10 9 notbid 
 |-  ( x = A -> ( -. B R x <-> -. B R A ) )
11 simprr 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> A =/= B )
12 simpl1 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> R e. TosetRel )
13 tsrps 
 |-  ( R e. TosetRel -> R e. PosetRel )
14 12 13 syl 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> R e. PosetRel )
15 simprl 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> A R B )
16 psasym 
 |-  ( ( R e. PosetRel /\ A R B /\ B R A ) -> A = B )
17 16 3expia 
 |-  ( ( R e. PosetRel /\ A R B ) -> ( B R A -> A = B ) )
18 14 15 17 syl2anc 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> ( B R A -> A = B ) )
19 18 necon3ad 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> ( A =/= B -> -. B R A ) )
20 11 19 mpd 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> -. B R A )
21 20 adantr 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> -. B R A )
22 10 6 21 elrabd 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> A e. { x e. X | -. B R x } )
23 breq1 
 |-  ( x = B -> ( x R A <-> B R A ) )
24 23 notbid 
 |-  ( x = B -> ( -. x R A <-> -. B R A ) )
25 24 3 21 elrabd 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> B e. { x e. X | -. x R A } )
26 simpr 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> { x e. X | ( -. B R x /\ -. x R A ) } = (/) )
27 eleq2 
 |-  ( m = { x e. X | -. B R x } -> ( A e. m <-> A e. { x e. X | -. B R x } ) )
28 ineq1 
 |-  ( m = { x e. X | -. B R x } -> ( m i^i n ) = ( { x e. X | -. B R x } i^i n ) )
29 28 eqeq1d 
 |-  ( m = { x e. X | -. B R x } -> ( ( m i^i n ) = (/) <-> ( { x e. X | -. B R x } i^i n ) = (/) ) )
30 27 29 3anbi13d 
 |-  ( m = { x e. X | -. B R x } -> ( ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) <-> ( A e. { x e. X | -. B R x } /\ B e. n /\ ( { x e. X | -. B R x } i^i n ) = (/) ) ) )
31 eleq2 
 |-  ( n = { x e. X | -. x R A } -> ( B e. n <-> B e. { x e. X | -. x R A } ) )
32 ineq2 
 |-  ( n = { x e. X | -. x R A } -> ( { x e. X | -. B R x } i^i n ) = ( { x e. X | -. B R x } i^i { x e. X | -. x R A } ) )
33 inrab 
 |-  ( { x e. X | -. B R x } i^i { x e. X | -. x R A } ) = { x e. X | ( -. B R x /\ -. x R A ) }
34 32 33 eqtrdi 
 |-  ( n = { x e. X | -. x R A } -> ( { x e. X | -. B R x } i^i n ) = { x e. X | ( -. B R x /\ -. x R A ) } )
35 34 eqeq1d 
 |-  ( n = { x e. X | -. x R A } -> ( ( { x e. X | -. B R x } i^i n ) = (/) <-> { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) )
36 31 35 3anbi23d 
 |-  ( n = { x e. X | -. x R A } -> ( ( A e. { x e. X | -. B R x } /\ B e. n /\ ( { x e. X | -. B R x } i^i n ) = (/) ) <-> ( A e. { x e. X | -. B R x } /\ B e. { x e. X | -. x R A } /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) ) )
37 30 36 rspc2ev 
 |-  ( ( { x e. X | -. B R x } e. ( ordTop ` R ) /\ { x e. X | -. x R A } e. ( ordTop ` R ) /\ ( A e. { x e. X | -. B R x } /\ B e. { x e. X | -. x R A } /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) ) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) )
38 5 8 22 25 26 37 syl113anc 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ { x e. X | ( -. B R x /\ -. x R A ) } = (/) ) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) )
39 38 ex 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> ( { x e. X | ( -. B R x /\ -. x R A ) } = (/) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) ) )
40 rabn0 
 |-  ( { x e. X | ( -. B R x /\ -. x R A ) } =/= (/) <-> E. x e. X ( -. B R x /\ -. x R A ) )
41 simpll1 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> R e. TosetRel )
42 simprl 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> x e. X )
43 1 ordtopn2 
 |-  ( ( R e. TosetRel /\ x e. X ) -> { y e. X | -. x R y } e. ( ordTop ` R ) )
44 41 42 43 syl2anc 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> { y e. X | -. x R y } e. ( ordTop ` R ) )
45 1 ordtopn1 
 |-  ( ( R e. TosetRel /\ x e. X ) -> { y e. X | -. y R x } e. ( ordTop ` R ) )
46 41 42 45 syl2anc 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> { y e. X | -. y R x } e. ( ordTop ` R ) )
47 breq2 
 |-  ( y = A -> ( x R y <-> x R A ) )
48 47 notbid 
 |-  ( y = A -> ( -. x R y <-> -. x R A ) )
49 simpll2 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> A e. X )
50 simprrr 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> -. x R A )
51 48 49 50 elrabd 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> A e. { y e. X | -. x R y } )
52 breq1 
 |-  ( y = B -> ( y R x <-> B R x ) )
53 52 notbid 
 |-  ( y = B -> ( -. y R x <-> -. B R x ) )
54 simpll3 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> B e. X )
55 simprrl 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> -. B R x )
56 53 54 55 elrabd 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> B e. { y e. X | -. y R x } )
57 41 42 jca 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> ( R e. TosetRel /\ x e. X ) )
58 1 tsrlin 
 |-  ( ( R e. TosetRel /\ x e. X /\ y e. X ) -> ( x R y \/ y R x ) )
59 58 3expa 
 |-  ( ( ( R e. TosetRel /\ x e. X ) /\ y e. X ) -> ( x R y \/ y R x ) )
60 57 59 sylan 
 |-  ( ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) /\ y e. X ) -> ( x R y \/ y R x ) )
61 oran 
 |-  ( ( x R y \/ y R x ) <-> -. ( -. x R y /\ -. y R x ) )
62 60 61 sylib 
 |-  ( ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) /\ y e. X ) -> -. ( -. x R y /\ -. y R x ) )
63 62 ralrimiva 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> A. y e. X -. ( -. x R y /\ -. y R x ) )
64 rabeq0 
 |-  ( { y e. X | ( -. x R y /\ -. y R x ) } = (/) <-> A. y e. X -. ( -. x R y /\ -. y R x ) )
65 63 64 sylibr 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> { y e. X | ( -. x R y /\ -. y R x ) } = (/) )
66 eleq2 
 |-  ( m = { y e. X | -. x R y } -> ( A e. m <-> A e. { y e. X | -. x R y } ) )
67 ineq1 
 |-  ( m = { y e. X | -. x R y } -> ( m i^i n ) = ( { y e. X | -. x R y } i^i n ) )
68 67 eqeq1d 
 |-  ( m = { y e. X | -. x R y } -> ( ( m i^i n ) = (/) <-> ( { y e. X | -. x R y } i^i n ) = (/) ) )
69 66 68 3anbi13d 
 |-  ( m = { y e. X | -. x R y } -> ( ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) <-> ( A e. { y e. X | -. x R y } /\ B e. n /\ ( { y e. X | -. x R y } i^i n ) = (/) ) ) )
70 eleq2 
 |-  ( n = { y e. X | -. y R x } -> ( B e. n <-> B e. { y e. X | -. y R x } ) )
71 ineq2 
 |-  ( n = { y e. X | -. y R x } -> ( { y e. X | -. x R y } i^i n ) = ( { y e. X | -. x R y } i^i { y e. X | -. y R x } ) )
72 inrab 
 |-  ( { y e. X | -. x R y } i^i { y e. X | -. y R x } ) = { y e. X | ( -. x R y /\ -. y R x ) }
73 71 72 eqtrdi 
 |-  ( n = { y e. X | -. y R x } -> ( { y e. X | -. x R y } i^i n ) = { y e. X | ( -. x R y /\ -. y R x ) } )
74 73 eqeq1d 
 |-  ( n = { y e. X | -. y R x } -> ( ( { y e. X | -. x R y } i^i n ) = (/) <-> { y e. X | ( -. x R y /\ -. y R x ) } = (/) ) )
75 70 74 3anbi23d 
 |-  ( n = { y e. X | -. y R x } -> ( ( A e. { y e. X | -. x R y } /\ B e. n /\ ( { y e. X | -. x R y } i^i n ) = (/) ) <-> ( A e. { y e. X | -. x R y } /\ B e. { y e. X | -. y R x } /\ { y e. X | ( -. x R y /\ -. y R x ) } = (/) ) ) )
76 69 75 rspc2ev 
 |-  ( ( { y e. X | -. x R y } e. ( ordTop ` R ) /\ { y e. X | -. y R x } e. ( ordTop ` R ) /\ ( A e. { y e. X | -. x R y } /\ B e. { y e. X | -. y R x } /\ { y e. X | ( -. x R y /\ -. y R x ) } = (/) ) ) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) )
77 44 46 51 56 65 76 syl113anc 
 |-  ( ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) /\ ( x e. X /\ ( -. B R x /\ -. x R A ) ) ) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) )
78 77 rexlimdvaa 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> ( E. x e. X ( -. B R x /\ -. x R A ) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) ) )
79 40 78 syl5bi 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> ( { x e. X | ( -. B R x /\ -. x R A ) } =/= (/) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) ) )
80 39 79 pm2.61dne 
 |-  ( ( ( R e. TosetRel /\ A e. X /\ B e. X ) /\ ( A R B /\ A =/= B ) ) -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) )
81 80 exp32 
 |-  ( ( R e. TosetRel /\ A e. X /\ B e. X ) -> ( A R B -> ( A =/= B -> E. m e. ( ordTop ` R ) E. n e. ( ordTop ` R ) ( A e. m /\ B e. n /\ ( m i^i n ) = (/) ) ) ) )