Theorem engch

Description: The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	engch	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ GCH ↔ 𝐵 ∈ GCH ) )

Proof

Step	Hyp	Ref	Expression
1		enfi	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
2		sdomen1	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ≺ 𝑥 ↔ 𝐵 ≺ 𝑥 ) )
3		pwen	⊢ ( 𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ 𝒫 𝐵 )
4		sdomen2	⊢ ( 𝒫 𝐴 ≈ 𝒫 𝐵 → ( 𝑥 ≺ 𝒫 𝐴 ↔ 𝑥 ≺ 𝒫 𝐵 ) )
5	3 4	syl	⊢ ( 𝐴 ≈ 𝐵 → ( 𝑥 ≺ 𝒫 𝐴 ↔ 𝑥 ≺ 𝒫 𝐵 ) )
6	2 5	anbi12d	⊢ ( 𝐴 ≈ 𝐵 → ( ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ↔ ( 𝐵 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐵 ) ) )
7	6	notbid	⊢ ( 𝐴 ≈ 𝐵 → ( ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ↔ ¬ ( 𝐵 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐵 ) ) )
8	7	albidv	⊢ ( 𝐴 ≈ 𝐵 → ( ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ↔ ∀ 𝑥 ¬ ( 𝐵 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐵 ) ) )
9	1 8	orbi12d	⊢ ( 𝐴 ≈ 𝐵 → ( ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ↔ ( 𝐵 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐵 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐵 ) ) ) )
10		relen	⊢ Rel ≈
11	10	brrelex1i	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
12		elgch	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) )
13	11 12	syl	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ GCH ↔ ( 𝐴 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴 ) ) ) )
14	10	brrelex2i	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
15		elgch	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ GCH ↔ ( 𝐵 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐵 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐵 ) ) ) )
16	14 15	syl	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐵 ∈ GCH ↔ ( 𝐵 ∈ Fin ∨ ∀ 𝑥 ¬ ( 𝐵 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐵 ) ) ) )
17	9 13 16	3bitr4d	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ GCH ↔ 𝐵 ∈ GCH ) )