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 ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2 1 con3i ⊢ ( ¬ 𝐴 ≼ 𝐵 → ¬ 𝐴 ≺ 𝐵 )
3 reldom ⊢ Rel ≼
4 3 brrelex1i ⊢ ( 𝐵 ≼ 𝒫 𝐴 → 𝐵 ∈ V )
5 4 3ad2ant3 ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → 𝐵 ∈ V )
6 fidomtri2 ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ Fin ) → ( 𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵 ) )
7 5 6 sylan ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ 𝐴 ∈ Fin ) → ( 𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵 ) )
8 2 7 syl5ibr ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ 𝐴 ∈ Fin ) → ( ¬ 𝐴 ≼ 𝐵 → 𝐵 ≼ 𝐴 ) )
9 8 orrd ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ 𝐴 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )
10 simp1 ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → 𝐴 ∈ GCH )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ∈ GCH )
12 simpr ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ¬ 𝐴 ∈ Fin ) → ¬ 𝐴 ∈ Fin )
13 djudoml ⊢ ( ( 𝐴 ∈ GCH ∧ 𝐵 ∈ V ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
14 10 5 13 syl2anc ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
16 djulepw ⊢ ( ( ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝒫 𝐴 )
17 16 3adant1 ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝒫 𝐴 )
18 17 adantr ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝒫 𝐴 )
19 gchor ⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≼ 𝒫 𝐴 ) ) → ( 𝐴 ≈ ( 𝐴 ⊔ 𝐵 ) ∨ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) )
20 11 12 15 18 19 syl22anc ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≈ ( 𝐴 ⊔ 𝐵 ) ∨ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) )
21 djudoml ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ GCH ) → 𝐵 ≼ ( 𝐵 ⊔ 𝐴 ) )
22 5 10 21 syl2anc ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → 𝐵 ≼ ( 𝐵 ⊔ 𝐴 ) )
23 djucomen ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ GCH ) → ( 𝐵 ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ 𝐵 ) )
24 5 10 23 syl2anc ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → ( 𝐵 ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ 𝐵 ) )
25 domentr ⊢ ( ( 𝐵 ≼ ( 𝐵 ⊔ 𝐴 ) ∧ ( 𝐵 ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ 𝐵 ) ) → 𝐵 ≼ ( 𝐴 ⊔ 𝐵 ) )
26 22 24 25 syl2anc ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → 𝐵 ≼ ( 𝐴 ⊔ 𝐵 ) )
27 domen2 ⊢ ( 𝐴 ≈ ( 𝐴 ⊔ 𝐵 ) → ( 𝐵 ≼ 𝐴 ↔ 𝐵 ≼ ( 𝐴 ⊔ 𝐵 ) ) )
28 26 27 syl5ibrcom ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → ( 𝐴 ≈ ( 𝐴 ⊔ 𝐵 ) → 𝐵 ≼ 𝐴 ) )
29 28 imp ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ 𝐴 ≈ ( 𝐴 ⊔ 𝐵 ) ) → 𝐵 ≼ 𝐴 )
30 29 olcd ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ 𝐴 ≈ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )
31 simpl1 ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → 𝐴 ∈ GCH )
32 canth2g ⊢ ( 𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴 )
33 sdomdom ⊢ ( 𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴 )
34 31 32 33 3syl ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → 𝐴 ≼ 𝒫 𝐴 )
35 simpl2 ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 )
36 pwen ⊢ ( ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 → 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 )
37 35 36 syl ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 )
38 enen2 ⊢ ( ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 → ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ 𝐵 ) ↔ 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 ) )
39 38 adantl ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ 𝐵 ) ↔ 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 ) )
40 37 39 mpbird ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ 𝐵 ) )
41 endom ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ 𝐵 ) → 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) )
42 pwdjudom ⊢ ( 𝒫 ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ 𝐵 ) → 𝒫 𝐴 ≼ 𝐵 )
43 40 41 42 3syl ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → 𝒫 𝐴 ≼ 𝐵 )
44 domtr ⊢ ( ( 𝐴 ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ 𝐵 ) → 𝐴 ≼ 𝐵 )
45 34 43 44 syl2anc ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → 𝐴 ≼ 𝐵 )
46 45 orcd ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )
47 30 46 jaodan ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ( 𝐴 ≈ ( 𝐴 ⊔ 𝐵 ) ∨ ( 𝐴 ⊔ 𝐵 ) ≈ 𝒫 𝐴 ) ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )
48 20 47 syldan ⊢ ( ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )
49 9 48 pm2.61dan ⊢ ( ( 𝐴 ∈ GCH ∧ ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )