hsmexlem4

Description: Lemma for hsmex . The core induction, establishing bounds on the order types of iterated unions of the initial set. (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	hsmexlem4	$⊢ (c \in ω \land d \in S) \to dom O \in H (c)$

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		fveq2	$⊢ c = \emptyset \to U (d) (c) = U (d) (\emptyset)$
7	6	imaeq2d	$⊢ c = \emptyset \to rank [U (d) (c)] = rank [U (d) (\emptyset)]$
8		oieq2	$⊢ rank [U (d) (c)] = rank [U (d) (\emptyset)] \to OrdIso (E, rank [U (d) (c)]) = OrdIso (E, rank [U (d) (\emptyset)])$
9	7 8	syl	$⊢ c = \emptyset \to OrdIso (E, rank [U (d) (c)]) = OrdIso (E, rank [U (d) (\emptyset)])$
10	5 9	eqtrid	$⊢ c = \emptyset \to O = OrdIso (E, rank [U (d) (\emptyset)])$
11	10	dmeqd	$⊢ c = \emptyset \to dom O = dom OrdIso (E, rank [U (d) (\emptyset)])$
12		fveq2	$⊢ c = \emptyset \to H (c) = H (\emptyset)$
13	11 12	eleq12d	$⊢ c = \emptyset \to (dom O \in H (c) \leftrightarrow dom OrdIso (E, rank [U (d) (\emptyset)]) \in H (\emptyset))$
14	13	ralbidv	$⊢ c = \emptyset \to (\forall d \in S dom O \in H (c) \leftrightarrow \forall d \in S dom OrdIso (E, rank [U (d) (\emptyset)]) \in H (\emptyset))$
15		fveq2	$⊢ c = e \to U (d) (c) = U (d) (e)$
16	15	imaeq2d	$⊢ c = e \to rank [U (d) (c)] = rank [U (d) (e)]$
17		oieq2	$⊢ rank [U (d) (c)] = rank [U (d) (e)] \to OrdIso (E, rank [U (d) (c)]) = OrdIso (E, rank [U (d) (e)])$
18	16 17	syl	$⊢ c = e \to OrdIso (E, rank [U (d) (c)]) = OrdIso (E, rank [U (d) (e)])$
19	5 18	eqtrid	$⊢ c = e \to O = OrdIso (E, rank [U (d) (e)])$
20	19	dmeqd	$⊢ c = e \to dom O = dom OrdIso (E, rank [U (d) (e)])$
21		fveq2	$⊢ c = e \to H (c) = H (e)$
22	20 21	eleq12d	$⊢ c = e \to (dom O \in H (c) \leftrightarrow dom OrdIso (E, rank [U (d) (e)]) \in H (e))$
23	22	ralbidv	$⊢ c = e \to (\forall d \in S dom O \in H (c) \leftrightarrow \forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e))$
24		fveq2	$⊢ c = suc e \to U (d) (c) = U (d) (suc e)$
25	24	imaeq2d	$⊢ c = suc e \to rank [U (d) (c)] = rank [U (d) (suc e)]$
26		oieq2	$⊢ rank [U (d) (c)] = rank [U (d) (suc e)] \to OrdIso (E, rank [U (d) (c)]) = OrdIso (E, rank [U (d) (suc e)])$
27	25 26	syl	$⊢ c = suc e \to OrdIso (E, rank [U (d) (c)]) = OrdIso (E, rank [U (d) (suc e)])$
28	5 27	eqtrid	$⊢ c = suc e \to O = OrdIso (E, rank [U (d) (suc e)])$
29	28	dmeqd	$⊢ c = suc e \to dom O = dom OrdIso (E, rank [U (d) (suc e)])$
30		fveq2	$⊢ c = suc e \to H (c) = H (suc e)$
31	29 30	eleq12d	$⊢ c = suc e \to (dom O \in H (c) \leftrightarrow dom OrdIso (E, rank [U (d) (suc e)]) \in H (suc e))$
32	31	ralbidv	$⊢ c = suc e \to (\forall d \in S dom O \in H (c) \leftrightarrow \forall d \in S dom OrdIso (E, rank [U (d) (suc e)]) \in H (suc e))$
33		imassrn	$⊢ rank [U (d) (\emptyset)] \subseteq ran rank$
34		rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$
35		frn	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to ran rank \subseteq On$
36	34 35	ax-mp	$⊢ ran rank \subseteq On$
37	33 36	sstri	$⊢ rank [U (d) (\emptyset)] \subseteq On$
38	3	ituni0	$⊢ d \in V \to U (d) (\emptyset) = d$
39	38	elv	$⊢ U (d) (\emptyset) = d$
40	39	imaeq2i	$⊢ rank [U (d) (\emptyset)] = rank [d]$
41		ffun	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to Fun rank$
42	34 41	ax-mp	$⊢ Fun rank$
43		vex	$⊢ d \in V$
44		wdomimag	$⊢ (Fun rank \land d \in V) \to rank [d] ≼^{*} d$
45	42 43 44	mp2an	$⊢ rank [d] ≼^{*} d$
46		sneq	$⊢ a = d \to \{a\} = \{d\}$
47	46	fveq2d	$⊢ a = d \to TC (\{a\}) = TC (\{d\})$
48	47	raleqdv	$⊢ a = d \to (\forall b \in TC (\{a\}) b ≼ X \leftrightarrow \forall b \in TC (\{d\}) b ≼ X)$
49	48 4	elrab2	$⊢ d \in S \leftrightarrow (d \in ⋃ R_{1} [On] \land \forall b \in TC (\{d\}) b ≼ X)$
50	49	simprbi	$⊢ d \in S \to \forall b \in TC (\{d\}) b ≼ X$
51		snex	$⊢ \{d\} \in V$
52		tcid	$⊢ \{d\} \in V \to \{d\} \subseteq TC (\{d\})$
53	51 52	ax-mp	$⊢ \{d\} \subseteq TC (\{d\})$
54		vsnid	$⊢ d \in \{d\}$
55	53 54	sselii	$⊢ d \in TC (\{d\})$
56		breq1	$⊢ b = d \to (b ≼ X \leftrightarrow d ≼ X)$
57	56	rspcv	$⊢ d \in TC (\{d\}) \to (\forall b \in TC (\{d\}) b ≼ X \to d ≼ X)$
58	55 57	ax-mp	$⊢ \forall b \in TC (\{d\}) b ≼ X \to d ≼ X$
59		domwdom	$⊢ d ≼ X \to d ≼^{*} X$
60	50 58 59	3syl	$⊢ d \in S \to d ≼^{*} X$
61		wdomtr	$⊢ (rank [d] ≼^{} d \land d ≼^{} X) \to rank [d] ≼^{*} X$
62	45 60 61	sylancr	$⊢ d \in S \to rank [d] ≼^{*} X$
63	40 62	eqbrtrid	$⊢ d \in S \to rank [U (d) (\emptyset)] ≼^{*} X$
64		eqid	$⊢ OrdIso (E, rank [U (d) (\emptyset)]) = OrdIso (E, rank [U (d) (\emptyset)])$
65	64	hsmexlem1	$⊢ (rank [U (d) (\emptyset)] \subseteq On \land rank [U (d) (\emptyset)] ≼^{*} X) \to dom OrdIso (E, rank [U (d) (\emptyset)]) \in har (𝒫 X)$
66	37 63 65	sylancr	$⊢ d \in S \to dom OrdIso (E, rank [U (d) (\emptyset)]) \in har (𝒫 X)$
67	2	hsmexlem7	$⊢ H (\emptyset) = har (𝒫 X)$
68	66 67	eleqtrrdi	$⊢ d \in S \to dom OrdIso (E, rank [U (d) (\emptyset)]) \in H (\emptyset)$
69	68	rgen	$⊢ \forall d \in S dom OrdIso (E, rank [U (d) (\emptyset)]) \in H (\emptyset)$
70		nfra1	$⊢ Ⅎ d \forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e)$
71		nfv	$⊢ Ⅎ d e \in ω$
72	70 71	nfan	$⊢ Ⅎ d (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land e \in ω)$
73	3	ituniiun	$⊢ d \in V \to U (d) (suc e) = ⋃_{f \in d} U (f) (e)$
74	73	elv	$⊢ U (d) (suc e) = ⋃_{f \in d} U (f) (e)$
75	74	imaeq2i	$⊢ rank [U (d) (suc e)] = rank [⋃_{f \in d} U (f) (e)]$
76		imaiun	$⊢ rank [⋃_{f \in d} U (f) (e)] = ⋃_{f \in d} rank [U (f) (e)]$
77	75 76	eqtri	$⊢ rank [U (d) (suc e)] = ⋃_{f \in d} rank [U (f) (e)]$
78		oieq2	$⊢ rank [U (d) (suc e)] = ⋃_{f \in d} rank [U (f) (e)] \to OrdIso (E, rank [U (d) (suc e)]) = OrdIso (E, ⋃_{f \in d} rank [U (f) (e)])$
79	77 78	ax-mp	$⊢ OrdIso (E, rank [U (d) (suc e)]) = OrdIso (E, ⋃_{f \in d} rank [U (f) (e)])$
80	79	dmeqi	$⊢ dom OrdIso (E, rank [U (d) (suc e)]) = dom OrdIso (E, ⋃_{f \in d} rank [U (f) (e)])$
81	60	ad2antll	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \to d ≼^{*} X$
82	2	hsmexlem9	$⊢ e \in ω \to H (e) \in On$
83	82	ad2antrl	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \to H (e) \in On$
84		fveq2	$⊢ d = f \to U (d) = U (f)$
85	84	fveq1d	$⊢ d = f \to U (d) (e) = U (f) (e)$
86	85	imaeq2d	$⊢ d = f \to rank [U (d) (e)] = rank [U (f) (e)]$
87		oieq2	$⊢ rank [U (d) (e)] = rank [U (f) (e)] \to OrdIso (E, rank [U (d) (e)]) = OrdIso (E, rank [U (f) (e)])$
88	86 87	syl	$⊢ d = f \to OrdIso (E, rank [U (d) (e)]) = OrdIso (E, rank [U (f) (e)])$
89	88	dmeqd	$⊢ d = f \to dom OrdIso (E, rank [U (d) (e)]) = dom OrdIso (E, rank [U (f) (e)])$
90	89	eleq1d	$⊢ d = f \to (dom OrdIso (E, rank [U (d) (e)]) \in H (e) \leftrightarrow dom OrdIso (E, rank [U (f) (e)]) \in H (e))$
91		simpll	$⊢ ((\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \land f \in d) \to \forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e)$
92	4	ssrab3	$⊢ S \subseteq ⋃ R_{1} [On]$
93	92	sseli	$⊢ d \in S \to d \in ⋃ R_{1} [On]$
94		r1elssi	$⊢ d \in ⋃ R_{1} [On] \to d \subseteq ⋃ R_{1} [On]$
95	93 94	syl	$⊢ d \in S \to d \subseteq ⋃ R_{1} [On]$
96	95	sselda	$⊢ (d \in S \land f \in d) \to f \in ⋃ R_{1} [On]$
97		snssi	$⊢ f \in d \to \{f\} \subseteq d$
98	43	tcss	$⊢ \{f\} \subseteq d \to TC (\{f\}) \subseteq TC (d)$
99	97 98	syl	$⊢ f \in d \to TC (\{f\}) \subseteq TC (d)$
100	51	tcel	$⊢ d \in \{d\} \to TC (d) \subseteq TC (\{d\})$
101	54 100	mp1i	$⊢ f \in d \to TC (d) \subseteq TC (\{d\})$
102	99 101	sstrd	$⊢ f \in d \to TC (\{f\}) \subseteq TC (\{d\})$
103		ssralv	$⊢ TC (\{f\}) \subseteq TC (\{d\}) \to (\forall b \in TC (\{d\}) b ≼ X \to \forall b \in TC (\{f\}) b ≼ X)$
104	102 103	syl	$⊢ f \in d \to (\forall b \in TC (\{d\}) b ≼ X \to \forall b \in TC (\{f\}) b ≼ X)$
105	50 104	mpan9	$⊢ (d \in S \land f \in d) \to \forall b \in TC (\{f\}) b ≼ X$
106		sneq	$⊢ a = f \to \{a\} = \{f\}$
107	106	fveq2d	$⊢ a = f \to TC (\{a\}) = TC (\{f\})$
108	107	raleqdv	$⊢ a = f \to (\forall b \in TC (\{a\}) b ≼ X \leftrightarrow \forall b \in TC (\{f\}) b ≼ X)$
109	108 4	elrab2	$⊢ f \in S \leftrightarrow (f \in ⋃ R_{1} [On] \land \forall b \in TC (\{f\}) b ≼ X)$
110	96 105 109	sylanbrc	$⊢ (d \in S \land f \in d) \to f \in S$
111	110	adantll	$⊢ ((e \in ω \land d \in S) \land f \in d) \to f \in S$
112	111	adantll	$⊢ ((\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \land f \in d) \to f \in S$
113	90 91 112	rspcdva	$⊢ ((\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \land f \in d) \to dom OrdIso (E, rank [U (f) (e)]) \in H (e)$
114		imassrn	$⊢ rank [U (f) (e)] \subseteq ran rank$
115	114 36	sstri	$⊢ rank [U (f) (e)] \subseteq On$
116		fvex	$⊢ U (f) (e) \in V$
117	116	funimaex	$⊢ Fun rank \to rank [U (f) (e)] \in V$
118	42 117	ax-mp	$⊢ rank [U (f) (e)] \in V$
119	118	elpw	$⊢ rank [U (f) (e)] \in 𝒫 On \leftrightarrow rank [U (f) (e)] \subseteq On$
120	115 119	mpbir	$⊢ rank [U (f) (e)] \in 𝒫 On$
121	113 120	jctil	$⊢ ((\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \land f \in d) \to (rank [U (f) (e)] \in 𝒫 On \land dom OrdIso (E, rank [U (f) (e)]) \in H (e))$
122	121	ralrimiva	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \to \forall f \in d (rank [U (f) (e)] \in 𝒫 On \land dom OrdIso (E, rank [U (f) (e)]) \in H (e))$
123		eqid	$⊢ OrdIso (E, rank [U (f) (e)]) = OrdIso (E, rank [U (f) (e)])$
124		eqid	$⊢ OrdIso (E, ⋃_{f \in d} rank [U (f) (e)]) = OrdIso (E, ⋃_{f \in d} rank [U (f) (e)])$
125	123 124	hsmexlem3	$⊢ ((d ≼^{*} X \land H (e) \in On) \land \forall f \in d (rank [U (f) (e)] \in 𝒫 On \land dom OrdIso (E, rank [U (f) (e)]) \in H (e))) \to dom OrdIso (E, ⋃_{f \in d} rank [U (f) (e)]) \in har (𝒫 (X \times H (e)))$
126	81 83 122 125	syl21anc	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \to dom OrdIso (E, ⋃_{f \in d} rank [U (f) (e)]) \in har (𝒫 (X \times H (e)))$
127	80 126	eqeltrid	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \to dom OrdIso (E, rank [U (d) (suc e)]) \in har (𝒫 (X \times H (e)))$
128	2	hsmexlem8	$⊢ e \in ω \to H (suc e) = har (𝒫 (X \times H (e)))$
129	128	ad2antrl	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \to H (suc e) = har (𝒫 (X \times H (e)))$
130	127 129	eleqtrrd	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land (e \in ω \land d \in S)) \to dom OrdIso (E, rank [U (d) (suc e)]) \in H (suc e)$
131	130	expr	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land e \in ω) \to (d \in S \to dom OrdIso (E, rank [U (d) (suc e)]) \in H (suc e))$
132	72 131	ralrimi	$⊢ (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \land e \in ω) \to \forall d \in S dom OrdIso (E, rank [U (d) (suc e)]) \in H (suc e)$
133	132	expcom	$⊢ e \in ω \to (\forall d \in S dom OrdIso (E, rank [U (d) (e)]) \in H (e) \to \forall d \in S dom OrdIso (E, rank [U (d) (suc e)]) \in H (suc e))$
134	14 23 32 69 133	finds1	$⊢ c \in ω \to \forall d \in S dom O \in H (c)$
135	134	r19.21bi	$⊢ (c \in ω \land d \in S) \to dom O \in H (c)$

Metamath Proof Explorer

Theorem hsmexlem4

Proof