hsmexlem1

Description: Lemma for hsmex . Bound the order type of a limited-cardinality set of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Hypothesis	hsmexlem.o	$⊢ O = OrdIso (E, A)$
	Assertion	hsmexlem1	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O \in har (𝒫 B)$

Proof

Step	Hyp	Ref	Expression
1		hsmexlem.o	$⊢ O = OrdIso (E, A)$
2	1	oicl	$⊢ Ord dom O$
3		relwdom	$⊢ Rel ≼^{*}$
4	3	brrelex1i	$⊢ A ≼^{*} B \to A \in V$
5	4	adantl	$⊢ (A \subseteq On \land A ≼^{*} B) \to A \in V$
6		uniexg	$⊢ A \in V \to ⋃ A \in V$
7		sucexg	$⊢ ⋃ A \in V \to suc ⋃ A \in V$
8	5 6 7	3syl	$⊢ (A \subseteq On \land A ≼^{*} B) \to suc ⋃ A \in V$
9	1	oif	$⊢ O : dom O ⟶ A$
10		onsucuni	$⊢ A \subseteq On \to A \subseteq suc ⋃ A$
11	10	adantr	$⊢ (A \subseteq On \land A ≼^{*} B) \to A \subseteq suc ⋃ A$
12		fss	$⊢ (O : dom O ⟶ A \land A \subseteq suc ⋃ A) \to O : dom O ⟶ suc ⋃ A$
13	9 11 12	sylancr	$⊢ (A \subseteq On \land A ≼^{*} B) \to O : dom O ⟶ suc ⋃ A$
14	1	oismo	$⊢ A \subseteq On \to (Smo O \land ran O = A)$
15	14	adantr	$⊢ (A \subseteq On \land A ≼^{*} B) \to (Smo O \land ran O = A)$
16	15	simpld	$⊢ (A \subseteq On \land A ≼^{*} B) \to Smo O$
17		ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$
18	17	adantr	$⊢ (A \subseteq On \land A ≼^{*} B) \to Ord ⋃ A$
19		ordsuc	$⊢ Ord ⋃ A \leftrightarrow Ord suc ⋃ A$
20	18 19	sylib	$⊢ (A \subseteq On \land A ≼^{*} B) \to Ord suc ⋃ A$
21		smorndom	$⊢ (O : dom O ⟶ suc ⋃ A \land Smo O \land Ord suc ⋃ A) \to dom O \subseteq suc ⋃ A$
22	13 16 20 21	syl3anc	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O \subseteq suc ⋃ A$
23	8 22	ssexd	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O \in V$
24		elong	$⊢ dom O \in V \to (dom O \in On \leftrightarrow Ord dom O)$
25	23 24	syl	$⊢ (A \subseteq On \land A ≼^{*} B) \to (dom O \in On \leftrightarrow Ord dom O)$
26	2 25	mpbiri	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O \in On$
27		canth2g	$⊢ dom O \in V \to dom O ≺ 𝒫 dom O$
28		sdomdom	$⊢ dom O ≺ 𝒫 dom O \to dom O ≼ 𝒫 dom O$
29	23 27 28	3syl	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O ≼ 𝒫 dom O$
30		simpl	$⊢ (A \subseteq On \land A ≼^{*} B) \to A \subseteq On$
31		epweon	$⊢ E We On$
32		wess	$⊢ A \subseteq On \to (E We On \to E We A)$
33	30 31 32	mpisyl	$⊢ (A \subseteq On \land A ≼^{*} B) \to E We A$
34		epse	$⊢ E Se A$
35	1	oiiso2	$⊢ (E We A \land E Se A) \to O {Isom}_{E, E} (dom O, ran O)$
36	33 34 35	sylancl	$⊢ (A \subseteq On \land A ≼^{*} B) \to O {Isom}_{E, E} (dom O, ran O)$
37		isof1o	$⊢ O {Isom}_{E, E} (dom O, ran O) \to O : dom O \underset{1-1 onto}{⟶} ran O$
38	36 37	syl	$⊢ (A \subseteq On \land A ≼^{*} B) \to O : dom O \underset{1-1 onto}{⟶} ran O$
39	15	simprd	$⊢ (A \subseteq On \land A ≼^{*} B) \to ran O = A$
40	39	f1oeq3d	$⊢ (A \subseteq On \land A ≼^{*} B) \to (O : dom O \underset{1-1 onto}{⟶} ran O \leftrightarrow O : dom O \underset{1-1 onto}{⟶} A)$
41	38 40	mpbid	$⊢ (A \subseteq On \land A ≼^{*} B) \to O : dom O \underset{1-1 onto}{⟶} A$
42		f1oen2g	$⊢ (dom O \in On \land A \in V \land O : dom O \underset{1-1 onto}{⟶} A) \to dom O \approx A$
43	26 5 41 42	syl3anc	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O \approx A$
44		endom	$⊢ dom O \approx A \to dom O ≼ A$
45		domwdom	$⊢ dom O ≼ A \to dom O ≼^{*} A$
46	43 44 45	3syl	$⊢ (A \subseteq On \land A ≼^{} B) \to dom O ≼^{} A$
47		wdomtr	$⊢ (dom O ≼^{} A \land A ≼^{} B) \to dom O ≼^{*} B$
48	46 47	sylancom	$⊢ (A \subseteq On \land A ≼^{} B) \to dom O ≼^{} B$
49		wdompwdom	$⊢ dom O ≼^{*} B \to 𝒫 dom O ≼ 𝒫 B$
50	48 49	syl	$⊢ (A \subseteq On \land A ≼^{*} B) \to 𝒫 dom O ≼ 𝒫 B$
51		domtr	$⊢ (dom O ≼ 𝒫 dom O \land 𝒫 dom O ≼ 𝒫 B) \to dom O ≼ 𝒫 B$
52	29 50 51	syl2anc	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O ≼ 𝒫 B$
53		elharval	$⊢ dom O \in har (𝒫 B) \leftrightarrow (dom O \in On \land dom O ≼ 𝒫 B)$
54	26 52 53	sylanbrc	$⊢ (A \subseteq On \land A ≼^{*} B) \to dom O \in har (𝒫 B)$

Metamath Proof Explorer

Theorem hsmexlem1

Proof