Theorem 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	⊢ 𝑂 = OrdIso ( E , 𝐴 )
Assertion	hsmexlem1	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵 ) → dom 𝑂 ∈ ( har ‘ 𝒫 𝐵 ) )

Proof

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