Theorem hauspwdom

Description: Simplify the cardinal A ^ NN of hausmapdom to ~P B = 2 ^ B when B is an infinite cardinal greater than A . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypothesis	hauspwdom.1	⊢ 𝑋 = ∪ 𝐽
Assertion	hauspwdom	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		hauspwdom.1	⊢ 𝑋 = ∪ 𝐽
2	1	hausmapdom	⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴 ↑m ℕ ) )
3	2	adantr	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴 ↑m ℕ ) )
4		simprr	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ℕ ≼ 𝐵 )
5		1nn	⊢ 1 ∈ ℕ
6		noel	⊢ ¬ 1 ∈ ∅
7		eleq2	⊢ ( ℕ = ∅ → ( 1 ∈ ℕ ↔ 1 ∈ ∅ ) )
8	6 7	mtbiri	⊢ ( ℕ = ∅ → ¬ 1 ∈ ℕ )
9	8	adantr	⊢ ( ( ℕ = ∅ ∧ 𝐴 = ∅ ) → ¬ 1 ∈ ℕ )
10	5 9	mt2	⊢ ¬ ( ℕ = ∅ ∧ 𝐴 = ∅ )
11		mapdom2	⊢ ( ( ℕ ≼ 𝐵 ∧ ¬ ( ℕ = ∅ ∧ 𝐴 = ∅ ) ) → ( 𝐴 ↑m ℕ ) ≼ ( 𝐴 ↑m 𝐵 ) )
12	4 10 11	sylancl	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 𝐴 ↑m ℕ ) ≼ ( 𝐴 ↑m 𝐵 ) )
13		sdomdom	⊢ ( 𝐴 ≺ 2o → 𝐴 ≼ 2o )
14	13	adantl	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → 𝐴 ≼ 2o )
15		mapdom1	⊢ ( 𝐴 ≼ 2o → ( 𝐴 ↑m 𝐵 ) ≼ ( 2o ↑m 𝐵 ) )
16	14 15	syl	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 𝐴 ↑m 𝐵 ) ≼ ( 2o ↑m 𝐵 ) )
17		reldom	⊢ Rel ≼
18	17	brrelex2i	⊢ ( ℕ ≼ 𝐵 → 𝐵 ∈ V )
19	18	ad2antll	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐵 ∈ V )
20		pw2eng	⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) )
21		ensym	⊢ ( 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
22	19 20 21	3syl	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
23	22	adantr	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
24		domentr	⊢ ( ( ( 𝐴 ↑m 𝐵 ) ≼ ( 2o ↑m 𝐵 ) ∧ ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
25	16 23 24	syl2anc	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
26		onfin2	⊢ ω = ( On ∩ Fin )
27		inss2	⊢ ( On ∩ Fin ) ⊆ Fin
28	26 27	eqsstri	⊢ ω ⊆ Fin
29		2onn	⊢ 2o ∈ ω
30	28 29	sselii	⊢ 2o ∈ Fin
31		simprl	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐴 ≼ 𝒫 𝐵 )
32	17	brrelex1i	⊢ ( 𝐴 ≼ 𝒫 𝐵 → 𝐴 ∈ V )
33	31 32	syl	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐴 ∈ V )
34		fidomtri	⊢ ( ( 2o ∈ Fin ∧ 𝐴 ∈ V ) → ( 2o ≼ 𝐴 ↔ ¬ 𝐴 ≺ 2o ) )
35	30 33 34	sylancr	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 2o ≼ 𝐴 ↔ ¬ 𝐴 ≺ 2o ) )
36	35	biimpar	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ ¬ 𝐴 ≺ 2o ) → 2o ≼ 𝐴 )
37		numth3	⊢ ( 𝐵 ∈ V → 𝐵 ∈ dom card )
38	19 37	syl	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐵 ∈ dom card )
39	38	adantr	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → 𝐵 ∈ dom card )
40		nnenom	⊢ ℕ ≈ ω
41	40	ensymi	⊢ ω ≈ ℕ
42		endomtr	⊢ ( ( ω ≈ ℕ ∧ ℕ ≼ 𝐵 ) → ω ≼ 𝐵 )
43	41 4 42	sylancr	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ω ≼ 𝐵 )
44	43	adantr	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → ω ≼ 𝐵 )
45		simpr	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → 2o ≼ 𝐴 )
46	31	adantr	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → 𝐴 ≼ 𝒫 𝐵 )
47		mappwen	⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴 ↑m 𝐵 ) ≈ 𝒫 𝐵 )
48	39 44 45 46 47	syl22anc	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → ( 𝐴 ↑m 𝐵 ) ≈ 𝒫 𝐵 )
49		endom	⊢ ( ( 𝐴 ↑m 𝐵 ) ≈ 𝒫 𝐵 → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
50	48 49	syl	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
51	36 50	syldan	⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ ¬ 𝐴 ≺ 2o ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
52	25 51	pm2.61dan	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
53		domtr	⊢ ( ( ( 𝐴 ↑m ℕ ) ≼ ( 𝐴 ↑m 𝐵 ) ∧ ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) → ( 𝐴 ↑m ℕ ) ≼ 𝒫 𝐵 )
54	12 52 53	syl2anc	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 𝐴 ↑m ℕ ) ≼ 𝒫 𝐵 )
55		domtr	⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴 ↑m ℕ ) ∧ ( 𝐴 ↑m ℕ ) ≼ 𝒫 𝐵 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 )
56	3 54 55	syl2anc	⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 )