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	$⊢ X = ⋃ J$
	Assertion	hauspwdom	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to cls (J) (A) ≼ 𝒫 B$

Proof

Step	Hyp	Ref	Expression
1		hauspwdom.1	$⊢ X = ⋃ J$
2	1	hausmapdom	$⊢ (J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \to cls (J) (A) ≼ (A^{ℕ})$
3	2	adantr	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to cls (J) (A) ≼ (A^{ℕ})$
4		simprr	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to ℕ ≼ B$
5		1nn	$⊢ 1 \in ℕ$
6		noel	$⊢ \neg 1 \in \emptyset$
7		eleq2	$⊢ ℕ = \emptyset \to (1 \in ℕ \leftrightarrow 1 \in \emptyset)$
8	6 7	mtbiri	$⊢ ℕ = \emptyset \to \neg 1 \in ℕ$
9	8	adantr	$⊢ (ℕ = \emptyset \land A = \emptyset) \to \neg 1 \in ℕ$
10	5 9	mt2	$⊢ \neg (ℕ = \emptyset \land A = \emptyset)$
11		mapdom2	$⊢ (ℕ ≼ B \land \neg (ℕ = \emptyset \land A = \emptyset)) \to (A^{ℕ}) ≼ (A^{B})$
12	4 10 11	sylancl	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to (A^{ℕ}) ≼ (A^{B})$
13		sdomdom	$⊢ A ≺ 2_{𝑜} \to A ≼ 2_{𝑜}$
14	13	adantl	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land A ≺ 2_{𝑜}) \to A ≼ 2_{𝑜}$
15		mapdom1	$⊢ A ≼ 2_{𝑜} \to (A^{B}) ≼ ({2_{𝑜}}^{B})$
16	14 15	syl	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land A ≺ 2_{𝑜}) \to (A^{B}) ≼ ({2_{𝑜}}^{B})$
17		reldom	$⊢ Rel ≼$
18	17	brrelex2i	$⊢ ℕ ≼ B \to B \in V$
19	18	ad2antll	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to B \in V$
20		pw2eng	$⊢ B \in V \to 𝒫 B \approx ({2_{𝑜}}^{B})$
21		ensym	$⊢ 𝒫 B \approx ({2_{𝑜}}^{B}) \to ({2_{𝑜}}^{B}) \approx 𝒫 B$
22	19 20 21	3syl	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to ({2_{𝑜}}^{B}) \approx 𝒫 B$
23	22	adantr	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land A ≺ 2_{𝑜}) \to ({2_{𝑜}}^{B}) \approx 𝒫 B$
24		domentr	$⊢ ((A^{B}) ≼ ({2_{𝑜}}^{B}) \land ({2_{𝑜}}^{B}) \approx 𝒫 B) \to (A^{B}) ≼ 𝒫 B$
25	16 23 24	syl2anc	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land A ≺ 2_{𝑜}) \to (A^{B}) ≼ 𝒫 B$
26		onfin2	$⊢ ω = On \cap Fin$
27		inss2	$⊢ On \cap Fin \subseteq Fin$
28	26 27	eqsstri	$⊢ ω \subseteq Fin$
29		2onn	$⊢ 2_{𝑜} \in ω$
30	28 29	sselii	$⊢ 2_{𝑜} \in Fin$
31		simprl	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to A ≼ 𝒫 B$
32	17	brrelex1i	$⊢ A ≼ 𝒫 B \to A \in V$
33	31 32	syl	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to A \in V$
34		fidomtri	$⊢ (2_{𝑜} \in Fin \land A \in V) \to (2_{𝑜} ≼ A \leftrightarrow \neg A ≺ 2_{𝑜})$
35	30 33 34	sylancr	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to (2_{𝑜} ≼ A \leftrightarrow \neg A ≺ 2_{𝑜})$
36	35	biimpar	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land \neg A ≺ 2_{𝑜}) \to 2_{𝑜} ≼ A$
37		numth3	$⊢ B \in V \to B \in dom card$
38	19 37	syl	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to B \in dom card$
39	38	adantr	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land 2_{𝑜} ≼ A) \to B \in dom card$
40		nnenom	$⊢ ℕ \approx ω$
41	40	ensymi	$⊢ ω \approx ℕ$
42		endomtr	$⊢ (ω \approx ℕ \land ℕ ≼ B) \to ω ≼ B$
43	41 4 42	sylancr	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to ω ≼ B$
44	43	adantr	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land 2_{𝑜} ≼ A) \to ω ≼ B$
45		simpr	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land 2_{𝑜} ≼ A) \to 2_{𝑜} ≼ A$
46	31	adantr	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land 2_{𝑜} ≼ A) \to A ≼ 𝒫 B$
47		mappwen	$⊢ ((B \in dom card \land ω ≼ B) \land (2_{𝑜} ≼ A \land A ≼ 𝒫 B)) \to (A^{B}) \approx 𝒫 B$
48	39 44 45 46 47	syl22anc	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land 2_{𝑜} ≼ A) \to (A^{B}) \approx 𝒫 B$
49		endom	$⊢ (A^{B}) \approx 𝒫 B \to (A^{B}) ≼ 𝒫 B$
50	48 49	syl	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land 2_{𝑜} ≼ A) \to (A^{B}) ≼ 𝒫 B$
51	36 50	syldan	$⊢ (((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \land \neg A ≺ 2_{𝑜}) \to (A^{B}) ≼ 𝒫 B$
52	25 51	pm2.61dan	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to (A^{B}) ≼ 𝒫 B$
53		domtr	$⊢ ((A^{ℕ}) ≼ (A^{B}) \land (A^{B}) ≼ 𝒫 B) \to (A^{ℕ}) ≼ 𝒫 B$
54	12 52 53	syl2anc	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to (A^{ℕ}) ≼ 𝒫 B$
55		domtr	$⊢ (cls (J) (A) ≼ (A^{ℕ}) \land (A^{ℕ}) ≼ 𝒫 B) \to cls (J) (A) ≼ 𝒫 B$
56	3 54 55	syl2anc	$⊢ ((J \in Haus \land J \in 1^{st} 𝜔 \land A \subseteq X) \land (A ≼ 𝒫 B \land ℕ ≼ B)) \to cls (J) (A) ≼ 𝒫 B$

Metamath Proof Explorer

Theorem hauspwdom

Proof