Theorem gchor

Description: If A <_ B <_ ~P A , and A is an infinite GCH-set, then either A = B or B = ~P A in cardinality. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	gchor	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴 ) ) → ( 𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		simprr	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴 ) ) → 𝐵 ≼ 𝒫 𝐴 )
2		brdom2	⊢ ( 𝐵 ≼ 𝒫 𝐴 ↔ ( 𝐵 ≺ 𝒫 𝐴 ∨ 𝐵 ≈ 𝒫 𝐴 ) )
3	1 2	sylib	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴 ) ) → ( 𝐵 ≺ 𝒫 𝐴 ∨ 𝐵 ≈ 𝒫 𝐴 ) )
4		gchen1	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴 ) ) → 𝐴 ≈ 𝐵 )
5	4	expr	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 ≺ 𝒫 𝐴 → 𝐴 ≈ 𝐵 ) )
6	5	adantrr	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴 ) ) → ( 𝐵 ≺ 𝒫 𝐴 → 𝐴 ≈ 𝐵 ) )
7	6	orim1d	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴 ) ) → ( ( 𝐵 ≺ 𝒫 𝐴 ∨ 𝐵 ≈ 𝒫 𝐴 ) → ( 𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴 ) ) )
8	3 7	mpd	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴 ) ) → ( 𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴 ) )