This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gchdomtri

Description: Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gchdomtri 
|- ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A ~<_ B \/ B ~<_ A ) )

Proof

Step Hyp Ref Expression
1 sdomdom 
 |-  ( A ~< B -> A ~<_ B )
2 1 con3i 
 |-  ( -. A ~<_ B -> -. A ~< B )
3 reldom 
 |-  Rel ~<_
4 3 brrelex1i 
 |-  ( B ~<_ ~P A -> B e. _V )
5 4 3ad2ant3 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> B e. _V )
6 fidomtri2 
 |-  ( ( B e. _V /\ A e. Fin ) -> ( B ~<_ A <-> -. A ~< B ) )
7 5 6 sylan 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A e. Fin ) -> ( B ~<_ A <-> -. A ~< B ) )
8 2 7 imbitrrid 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A e. Fin ) -> ( -. A ~<_ B -> B ~<_ A ) )
9 8 orrd 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A e. Fin ) -> ( A ~<_ B \/ B ~<_ A ) )
10 simp1 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> A e. GCH )
11 10 adantr 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ -. A e. Fin ) -> A e. GCH )
12 simpr 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ -. A e. Fin ) -> -. A e. Fin )
13 djudoml 
 |-  ( ( A e. GCH /\ B e. _V ) -> A ~<_ ( A |_| B ) )
14 10 5 13 syl2anc 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> A ~<_ ( A |_| B ) )
15 14 adantr 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ -. A e. Fin ) -> A ~<_ ( A |_| B ) )
16 djulepw 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ~P A )
17 16 3adant1 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ~P A )
18 17 adantr 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ -. A e. Fin ) -> ( A |_| B ) ~<_ ~P A )
19 gchor 
 |-  ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ ( A |_| B ) /\ ( A |_| B ) ~<_ ~P A ) ) -> ( A ~~ ( A |_| B ) \/ ( A |_| B ) ~~ ~P A ) )
20 11 12 15 18 19 syl22anc 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ -. A e. Fin ) -> ( A ~~ ( A |_| B ) \/ ( A |_| B ) ~~ ~P A ) )
21 djudoml 
 |-  ( ( B e. _V /\ A e. GCH ) -> B ~<_ ( B |_| A ) )
22 5 10 21 syl2anc 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> B ~<_ ( B |_| A ) )
23 djucomen 
 |-  ( ( B e. _V /\ A e. GCH ) -> ( B |_| A ) ~~ ( A |_| B ) )
24 5 10 23 syl2anc 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( B |_| A ) ~~ ( A |_| B ) )
25 domentr 
 |-  ( ( B ~<_ ( B |_| A ) /\ ( B |_| A ) ~~ ( A |_| B ) ) -> B ~<_ ( A |_| B ) )
26 22 24 25 syl2anc 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> B ~<_ ( A |_| B ) )
27 domen2 
 |-  ( A ~~ ( A |_| B ) -> ( B ~<_ A <-> B ~<_ ( A |_| B ) ) )
28 26 27 syl5ibrcom 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A ~~ ( A |_| B ) -> B ~<_ A ) )
29 28 imp 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A ~~ ( A |_| B ) ) -> B ~<_ A )
30 29 olcd 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A ~~ ( A |_| B ) ) -> ( A ~<_ B \/ B ~<_ A ) )
31 simpl1 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> A e. GCH )
32 canth2g 
 |-  ( A e. GCH -> A ~< ~P A )
33 sdomdom 
 |-  ( A ~< ~P A -> A ~<_ ~P A )
34 31 32 33 3syl 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> A ~<_ ~P A )
35 simpl2 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> ( A |_| A ) ~~ A )
36 pwen 
 |-  ( ( A |_| A ) ~~ A -> ~P ( A |_| A ) ~~ ~P A )
37 35 36 syl 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> ~P ( A |_| A ) ~~ ~P A )
38 enen2 
 |-  ( ( A |_| B ) ~~ ~P A -> ( ~P ( A |_| A ) ~~ ( A |_| B ) <-> ~P ( A |_| A ) ~~ ~P A ) )
39 38 adantl 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> ( ~P ( A |_| A ) ~~ ( A |_| B ) <-> ~P ( A |_| A ) ~~ ~P A ) )
40 37 39 mpbird 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> ~P ( A |_| A ) ~~ ( A |_| B ) )
41 endom 
 |-  ( ~P ( A |_| A ) ~~ ( A |_| B ) -> ~P ( A |_| A ) ~<_ ( A |_| B ) )
42 pwdjudom 
 |-  ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ~P A ~<_ B )
43 40 41 42 3syl 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> ~P A ~<_ B )
44 domtr 
 |-  ( ( A ~<_ ~P A /\ ~P A ~<_ B ) -> A ~<_ B )
45 34 43 44 syl2anc 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> A ~<_ B )
46 45 orcd 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A |_| B ) ~~ ~P A ) -> ( A ~<_ B \/ B ~<_ A ) )
47 30 46 jaodan 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ ( A ~~ ( A |_| B ) \/ ( A |_| B ) ~~ ~P A ) ) -> ( A ~<_ B \/ B ~<_ A ) )
48 20 47 syldan 
 |-  ( ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ -. A e. Fin ) -> ( A ~<_ B \/ B ~<_ A ) )
49 9 48 pm2.61dan 
 |-  ( ( A e. GCH /\ ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A ~<_ B \/ B ~<_ A ) )