hsmexlem5

Description: Lemma for hsmex . Combining the above constraints, along with itunitc and tcrank , gives an effective constraint on the rank of S . (Contributed by Stefan O'Rear, 14-Feb-2015)

	Ref	Expression
Hypotheses	hsmexlem4.x	$⊢ X \in V$
	hsmexlem4.h	$⊢ H = {rec ((z \in V ⟼ har (𝒫 (X \times z))), har (𝒫 X)) ↾}_{ω}$
	hsmexlem4.u	$⊢ U = (x \in V ⟼ {rec ((y \in V ⟼ ⋃ y), x) ↾}_{ω})$
	hsmexlem4.s	$⊢ S = \{a \in ⋃ R_{1} [On] \| \forall b \in TC (\{a\}) b ≼ X\}$
	hsmexlem4.o	$⊢ O = OrdIso (E, rank [U (d) (c)])$
Assertion	hsmexlem5	$⊢ d \in S \to rank (d) \in har (𝒫 (ω \times ⋃ ran H))$

Proof

Step	Hyp	Ref	Expression
1		hsmexlem4.x	$⊢ X \in V$
2		hsmexlem4.h	$⊢ H = {rec ((z \in V ⟼ har (𝒫 (X \times z))), har (𝒫 X)) ↾}_{ω}$
3		hsmexlem4.u	$⊢ U = (x \in V ⟼ {rec ((y \in V ⟼ ⋃ y), x) ↾}_{ω})$
4		hsmexlem4.s	$⊢ S = \{a \in ⋃ R_{1} [On] \| \forall b \in TC (\{a\}) b ≼ X\}$
5		hsmexlem4.o	$⊢ O = OrdIso (E, rank [U (d) (c)])$
6	4	ssrab3	$⊢ S \subseteq ⋃ R_{1} [On]$
7	6	sseli	$⊢ d \in S \to d \in ⋃ R_{1} [On]$
8		tcrank	$⊢ d \in ⋃ R_{1} [On] \to rank (d) = rank [TC (d)]$
9	7 8	syl	$⊢ d \in S \to rank (d) = rank [TC (d)]$
10	3	itunitc	$⊢ TC (d) = ⋃ ran U (d)$
11	3	itunifn	$⊢ d \in S \to U (d) Fn ω$
12		fniunfv	$⊢ U (d) Fn ω \to ⋃_{c \in ω} U (d) (c) = ⋃ ran U (d)$
13	11 12	syl	$⊢ d \in S \to ⋃_{c \in ω} U (d) (c) = ⋃ ran U (d)$
14	10 13	eqtr4id	$⊢ d \in S \to TC (d) = ⋃_{c \in ω} U (d) (c)$
15	14	imaeq2d	$⊢ d \in S \to rank [TC (d)] = rank [⋃_{c \in ω} U (d) (c)]$
16		imaiun	$⊢ rank [⋃_{c \in ω} U (d) (c)] = ⋃_{c \in ω} rank [U (d) (c)]$
17	16	a1i	$⊢ d \in S \to rank [⋃_{c \in ω} U (d) (c)] = ⋃_{c \in ω} rank [U (d) (c)]$
18	9 15 17	3eqtrd	$⊢ d \in S \to rank (d) = ⋃_{c \in ω} rank [U (d) (c)]$
19		dmresi	$⊢ dom ({I ↾}_{⋃_{c \in ω} rank [U (d) (c)]}) = ⋃_{c \in ω} rank [U (d) (c)]$
20	18 19	eqtr4di	$⊢ d \in S \to rank (d) = dom ({I ↾}_{⋃_{c \in ω} rank [U (d) (c)]})$
21		rankon	$⊢ rank (d) \in On$
22	18 21	eqeltrrdi	$⊢ d \in S \to ⋃_{c \in ω} rank [U (d) (c)] \in On$
23		eloni	$⊢ ⋃_{c \in ω} rank [U (d) (c)] \in On \to Ord ⋃_{c \in ω} rank [U (d) (c)]$
24		oiid	$⊢ Ord ⋃_{c \in ω} rank [U (d) (c)] \to OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)]) = {I ↾}_{⋃_{c \in ω} rank [U (d) (c)]}$
25	22 23 24	3syl	$⊢ d \in S \to OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)]) = {I ↾}_{⋃_{c \in ω} rank [U (d) (c)]}$
26	25	dmeqd	$⊢ d \in S \to dom OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)]) = dom ({I ↾}_{⋃_{c \in ω} rank [U (d) (c)]})$
27	20 26	eqtr4d	$⊢ d \in S \to rank (d) = dom OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)])$
28		omex	$⊢ ω \in V$
29		wdomref	$⊢ ω \in V \to ω ≼^{*} ω$
30	28 29	mp1i	$⊢ d \in S \to ω ≼^{*} ω$
31		frfnom	$⊢ ({rec ((z \in V ⟼ har (𝒫 (X \times z))), har (𝒫 X)) ↾}_{ω}) Fn ω$
32	2	fneq1i	$⊢ H Fn ω \leftrightarrow ({rec ((z \in V ⟼ har (𝒫 (X \times z))), har (𝒫 X)) ↾}_{ω}) Fn ω$
33	31 32	mpbir	$⊢ H Fn ω$
34		fniunfv	$⊢ H Fn ω \to ⋃_{a \in ω} H (a) = ⋃ ran H$
35	33 34	ax-mp	$⊢ ⋃_{a \in ω} H (a) = ⋃ ran H$
36		iunon	$⊢ (ω \in V \land \forall a \in ω H (a) \in On) \to ⋃_{a \in ω} H (a) \in On$
37	28 36	mpan	$⊢ \forall a \in ω H (a) \in On \to ⋃_{a \in ω} H (a) \in On$
38	2	hsmexlem9	$⊢ a \in ω \to H (a) \in On$
39	37 38	mprg	$⊢ ⋃_{a \in ω} H (a) \in On$
40	35 39	eqeltrri	$⊢ ⋃ ran H \in On$
41	40	a1i	$⊢ d \in S \to ⋃ ran H \in On$
42		fvssunirn	$⊢ H (c) \subseteq ⋃ ran H$
43		eqid	$⊢ OrdIso (E, rank [U (d) (c)]) = OrdIso (E, rank [U (d) (c)])$
44	1 2 3 4 43	hsmexlem4	$⊢ (c \in ω \land d \in S) \to dom OrdIso (E, rank [U (d) (c)]) \in H (c)$
45	44	ancoms	$⊢ (d \in S \land c \in ω) \to dom OrdIso (E, rank [U (d) (c)]) \in H (c)$
46	42 45	sselid	$⊢ (d \in S \land c \in ω) \to dom OrdIso (E, rank [U (d) (c)]) \in ⋃ ran H$
47		imassrn	$⊢ rank [U (d) (c)] \subseteq ran rank$
48		rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$
49		frn	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to ran rank \subseteq On$
50	48 49	ax-mp	$⊢ ran rank \subseteq On$
51	47 50	sstri	$⊢ rank [U (d) (c)] \subseteq On$
52		ffun	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to Fun rank$
53		fvex	$⊢ U (d) (c) \in V$
54	53	funimaex	$⊢ Fun rank \to rank [U (d) (c)] \in V$
55	48 52 54	mp2b	$⊢ rank [U (d) (c)] \in V$
56	55	elpw	$⊢ rank [U (d) (c)] \in 𝒫 On \leftrightarrow rank [U (d) (c)] \subseteq On$
57	51 56	mpbir	$⊢ rank [U (d) (c)] \in 𝒫 On$
58	46 57	jctil	$⊢ (d \in S \land c \in ω) \to (rank [U (d) (c)] \in 𝒫 On \land dom OrdIso (E, rank [U (d) (c)]) \in ⋃ ran H)$
59	58	ralrimiva	$⊢ d \in S \to \forall c \in ω (rank [U (d) (c)] \in 𝒫 On \land dom OrdIso (E, rank [U (d) (c)]) \in ⋃ ran H)$
60		eqid	$⊢ OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)]) = OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)])$
61	43 60	hsmexlem3	$⊢ ((ω ≼^{*} ω \land ⋃ ran H \in On) \land \forall c \in ω (rank [U (d) (c)] \in 𝒫 On \land dom OrdIso (E, rank [U (d) (c)]) \in ⋃ ran H)) \to dom OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)]) \in har (𝒫 (ω \times ⋃ ran H))$
62	30 41 59 61	syl21anc	$⊢ d \in S \to dom OrdIso (E, ⋃_{c \in ω} rank [U (d) (c)]) \in har (𝒫 (ω \times ⋃ ran H))$
63	27 62	eqeltrd	$⊢ d \in S \to rank (d) \in har (𝒫 (ω \times ⋃ ran H))$

Metamath Proof Explorer

Theorem hsmexlem5

Proof