Metamath Proof Explorer

Theorem gchaclem

Description: Lemma for gchac (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses gchaclem.1 
|- ( ph -> _om ~<_ A )
gchaclem.3 
|- ( ph -> ~P C e. GCH )
gchaclem.4 
|- ( ph -> ( A ~<_ C /\ ( B ~<_ ~P C -> ~P A ~<_ B ) ) )
Assertion gchaclem 
|- ( ph -> ( A ~<_ ~P C /\ ( B ~<_ ~P ~P C -> ~P A ~<_ B ) ) )

Proof

Step Hyp Ref Expression
1 gchaclem.1 
 |-  ( ph -> _om ~<_ A )
2 gchaclem.3 
 |-  ( ph -> ~P C e. GCH )
3 gchaclem.4 
 |-  ( ph -> ( A ~<_ C /\ ( B ~<_ ~P C -> ~P A ~<_ B ) ) )
4 3 simpld 
 |-  ( ph -> A ~<_ C )
5 reldom 
 |-  Rel ~<_
6 5 brrelex2i 
 |-  ( A ~<_ C -> C e. _V )
7 4 6 syl 
 |-  ( ph -> C e. _V )
8 canth2g 
 |-  ( C e. _V -> C ~< ~P C )
9 sdomdom 
 |-  ( C ~< ~P C -> C ~<_ ~P C )
10 7 8 9 3syl 
 |-  ( ph -> C ~<_ ~P C )
11 domtr 
 |-  ( ( A ~<_ C /\ C ~<_ ~P C ) -> A ~<_ ~P C )
12 4 10 11 syl2anc 
 |-  ( ph -> A ~<_ ~P C )
13 2 adantr 
 |-  ( ( ph /\ B ~<_ ~P ~P C ) -> ~P C e. GCH )
14 domtr 
 |-  ( ( _om ~<_ A /\ A ~<_ C ) -> _om ~<_ C )
15 1 4 14 syl2anc 
 |-  ( ph -> _om ~<_ C )
16 15 adantr 
 |-  ( ( ph /\ B ~<_ ~P ~P C ) -> _om ~<_ C )
17 pwdjuidm 
 |-  ( _om ~<_ C -> ( ~P C |_| ~P C ) ~~ ~P C )
18 16 17 syl 
 |-  ( ( ph /\ B ~<_ ~P ~P C ) -> ( ~P C |_| ~P C ) ~~ ~P C )
19 simpr 
 |-  ( ( ph /\ B ~<_ ~P ~P C ) -> B ~<_ ~P ~P C )
20 gchdomtri 
 |-  ( ( ~P C e. GCH /\ ( ~P C |_| ~P C ) ~~ ~P C /\ B ~<_ ~P ~P C ) -> ( ~P C ~<_ B \/ B ~<_ ~P C ) )
21 13 18 19 20 syl3anc 
 |-  ( ( ph /\ B ~<_ ~P ~P C ) -> ( ~P C ~<_ B \/ B ~<_ ~P C ) )
22 21 ex 
 |-  ( ph -> ( B ~<_ ~P ~P C -> ( ~P C ~<_ B \/ B ~<_ ~P C ) ) )
23 pwdom 
 |-  ( A ~<_ C -> ~P A ~<_ ~P C )
24 domtr 
 |-  ( ( ~P A ~<_ ~P C /\ ~P C ~<_ B ) -> ~P A ~<_ B )
25 24 ex 
 |-  ( ~P A ~<_ ~P C -> ( ~P C ~<_ B -> ~P A ~<_ B ) )
26 4 23 25 3syl 
 |-  ( ph -> ( ~P C ~<_ B -> ~P A ~<_ B ) )
27 3 simprd 
 |-  ( ph -> ( B ~<_ ~P C -> ~P A ~<_ B ) )
28 26 27 jaod 
 |-  ( ph -> ( ( ~P C ~<_ B \/ B ~<_ ~P C ) -> ~P A ~<_ B ) )
29 22 28 syld 
 |-  ( ph -> ( B ~<_ ~P ~P C -> ~P A ~<_ B ) )
30 12 29 jca 
 |-  ( ph -> ( A ~<_ ~P C /\ ( B ~<_ ~P ~P C -> ~P A ~<_ B ) ) )