heiborlem3

Description: Lemma for heibor . Using countable choice ax-cc , we have fixed in advance a collection of finite 2 ^ -u n nets ( Fn ) for X (note that an r -net is a set of points in X whose r -balls cover X ). The set G is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set K ). If the theorem was false, then X would be in K , and so some ball at each level would also be in K . But we can say more than this; given a ball ( y B n ) on level n , since level n + 1 covers the space and thus also ( y B n ) , using heiborlem1 there is a ball on the next level whose intersection with ( y B n ) also has no finite subcover. Now since the set G is a countable union of finite sets, it is countable (which needs ax-cc via iunctb ), and so we can apply ax-cc to G directly to get a function from G to itself, which points from each ball in K to a ball on the next level in K , and such that the intersection between these balls is also in K . (Contributed by Jeff Madsen, 18-Jan-2014)

	Ref	Expression
Hypotheses	heibor.1	$⊢ J = MetOpen (D)$
	heibor.3	$⊢ K = \{u \| \neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v\}$
	heibor.4	$⊢ G = \{⟨y, n⟩ \| (n \in ℕ_{0} \land y \in F (n) \land y B n \in K)\}$
	heibor.5	$⊢ B = (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}}))$
	heibor.6	$⊢ φ \to D \in CMet (X)$
	heibor.7	$⊢ φ \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
	heibor.8	$⊢ φ \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
Assertion	heiborlem3	$⊢ φ \to \exists g \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)$

Proof

Step	Hyp	Ref	Expression
1		heibor.1	$⊢ J = MetOpen (D)$
2		heibor.3	$⊢ K = \{u \| \neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v\}$
3		heibor.4	$⊢ G = \{⟨y, n⟩ \| (n \in ℕ_{0} \land y \in F (n) \land y B n \in K)\}$
4		heibor.5	$⊢ B = (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}}))$
5		heibor.6	$⊢ φ \to D \in CMet (X)$
6		heibor.7	$⊢ φ \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
7		heibor.8	$⊢ φ \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
8		nn0ex	$⊢ ℕ_{0} \in V$
9		fvex	$⊢ F (t) \in V$
10		snex	$⊢ \{t\} \in V$
11	9 10	xpex	$⊢ F (t) \times \{t\} \in V$
12	8 11	iunex	$⊢ ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) \in V$
13	3	relopabiv	$⊢ Rel G$
14		1st2nd	$⊢ (Rel G \land x \in G) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
15	13 14	mpan	$⊢ x \in G \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
16	15	eleq1d	$⊢ x \in G \to (x \in G \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ \in G)$
17		df-br	$⊢ 1^{st} (x) G 2^{nd} (x) \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ \in G$
18	16 17	bitr4di	$⊢ x \in G \to (x \in G \leftrightarrow 1^{st} (x) G 2^{nd} (x))$
19		fvex	$⊢ 1^{st} (x) \in V$
20		fvex	$⊢ 2^{nd} (x) \in V$
21	1 2 3 19 20	heiborlem2	$⊢ 1^{st} (x) G 2^{nd} (x) \leftrightarrow (2^{nd} (x) \in ℕ_{0} \land 1^{st} (x) \in F (2^{nd} (x)) \land 1^{st} (x) B 2^{nd} (x) \in K)$
22	18 21	bitrdi	$⊢ x \in G \to (x \in G \leftrightarrow (2^{nd} (x) \in ℕ_{0} \land 1^{st} (x) \in F (2^{nd} (x)) \land 1^{st} (x) B 2^{nd} (x) \in K))$
23	22	ibi	$⊢ x \in G \to (2^{nd} (x) \in ℕ_{0} \land 1^{st} (x) \in F (2^{nd} (x)) \land 1^{st} (x) B 2^{nd} (x) \in K)$
24	20	snid	$⊢ 2^{nd} (x) \in \{2^{nd} (x)\}$
25		opelxp	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (2^{nd} (x)) \times \{2^{nd} (x)\}) \leftrightarrow (1^{st} (x) \in F (2^{nd} (x)) \land 2^{nd} (x) \in \{2^{nd} (x)\})$
26	24 25	mpbiran2	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (2^{nd} (x)) \times \{2^{nd} (x)\}) \leftrightarrow 1^{st} (x) \in F (2^{nd} (x))$
27		fveq2	$⊢ t = 2^{nd} (x) \to F (t) = F (2^{nd} (x))$
28		sneq	$⊢ t = 2^{nd} (x) \to \{t\} = \{2^{nd} (x)\}$
29	27 28	xpeq12d	$⊢ t = 2^{nd} (x) \to F (t) \times \{t\} = F (2^{nd} (x)) \times \{2^{nd} (x)\}$
30	29	eleq2d	$⊢ t = 2^{nd} (x) \to (⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (t) \times \{t\}) \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (2^{nd} (x)) \times \{2^{nd} (x)\}))$
31	30	rspcev	$⊢ (2^{nd} (x) \in ℕ_{0} \land ⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (2^{nd} (x)) \times \{2^{nd} (x)\})) \to \exists t \in ℕ_{0} ⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (t) \times \{t\})$
32	26 31	sylan2br	$⊢ (2^{nd} (x) \in ℕ_{0} \land 1^{st} (x) \in F (2^{nd} (x))) \to \exists t \in ℕ_{0} ⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (t) \times \{t\})$
33		eliun	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) \leftrightarrow \exists t \in ℕ_{0} ⟨1^{st} (x), 2^{nd} (x)⟩ \in (F (t) \times \{t\})$
34	32 33	sylibr	$⊢ (2^{nd} (x) \in ℕ_{0} \land 1^{st} (x) \in F (2^{nd} (x))) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in ⋃_{t \in ℕ_{0}} (F (t) \times \{t\})$
35	34	3adant3	$⊢ (2^{nd} (x) \in ℕ_{0} \land 1^{st} (x) \in F (2^{nd} (x)) \land 1^{st} (x) B 2^{nd} (x) \in K) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in ⋃_{t \in ℕ_{0}} (F (t) \times \{t\})$
36	23 35	syl	$⊢ x \in G \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in ⋃_{t \in ℕ_{0}} (F (t) \times \{t\})$
37	15 36	eqeltrd	$⊢ x \in G \to x \in ⋃_{t \in ℕ_{0}} (F (t) \times \{t\})$
38	37	ssriv	$⊢ G \subseteq ⋃_{t \in ℕ_{0}} (F (t) \times \{t\})$
39		ssdomg	$⊢ ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) \in V \to (G \subseteq ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) \to G ≼ ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}))$
40	12 38 39	mp2	$⊢ G ≼ ⋃_{t \in ℕ_{0}} (F (t) \times \{t\})$
41		nn0ennn	$⊢ ℕ_{0} \approx ℕ$
42		nnenom	$⊢ ℕ \approx ω$
43	41 42	entri	$⊢ ℕ_{0} \approx ω$
44		endom	$⊢ ℕ_{0} \approx ω \to ℕ_{0} ≼ ω$
45	43 44	ax-mp	$⊢ ℕ_{0} ≼ ω$
46		vex	$⊢ t \in V$
47	9 46	xpsnen	$⊢ (F (t) \times \{t\}) \approx F (t)$
48		inss2	$⊢ 𝒫 X \cap Fin \subseteq Fin$
49	6	ffvelrnda	$⊢ (φ \land t \in ℕ_{0}) \to F (t) \in (𝒫 X \cap Fin)$
50	48 49	sselid	$⊢ (φ \land t \in ℕ_{0}) \to F (t) \in Fin$
51		isfinite	$⊢ F (t) \in Fin \leftrightarrow F (t) ≺ ω$
52		sdomdom	$⊢ F (t) ≺ ω \to F (t) ≼ ω$
53	51 52	sylbi	$⊢ F (t) \in Fin \to F (t) ≼ ω$
54	50 53	syl	$⊢ (φ \land t \in ℕ_{0}) \to F (t) ≼ ω$
55		endomtr	$⊢ ((F (t) \times \{t\}) \approx F (t) \land F (t) ≼ ω) \to (F (t) \times \{t\}) ≼ ω$
56	47 54 55	sylancr	$⊢ (φ \land t \in ℕ_{0}) \to (F (t) \times \{t\}) ≼ ω$
57	56	ralrimiva	$⊢ φ \to \forall t \in ℕ_{0} (F (t) \times \{t\}) ≼ ω$
58		iunctb	$⊢ (ℕ_{0} ≼ ω \land \forall t \in ℕ_{0} (F (t) \times \{t\}) ≼ ω) \to ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) ≼ ω$
59	45 57 58	sylancr	$⊢ φ \to ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) ≼ ω$
60		domtr	$⊢ (G ≼ ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) \land ⋃_{t \in ℕ_{0}} (F (t) \times \{t\}) ≼ ω) \to G ≼ ω$
61	40 59 60	sylancr	$⊢ φ \to G ≼ ω$
62	23	simp1d	$⊢ x \in G \to 2^{nd} (x) \in ℕ_{0}$
63		peano2nn0	$⊢ 2^{nd} (x) \in ℕ_{0} \to 2^{nd} (x) + 1 \in ℕ_{0}$
64	62 63	syl	$⊢ x \in G \to 2^{nd} (x) + 1 \in ℕ_{0}$
65		ffvelrn	$⊢ (F : ℕ_{0} ⟶ 𝒫 X \cap Fin \land 2^{nd} (x) + 1 \in ℕ_{0}) \to F (2^{nd} (x) + 1) \in (𝒫 X \cap Fin)$
66	6 64 65	syl2an	$⊢ (φ \land x \in G) \to F (2^{nd} (x) + 1) \in (𝒫 X \cap Fin)$
67	48 66	sselid	$⊢ (φ \land x \in G) \to F (2^{nd} (x) + 1) \in Fin$
68		iunin2	$⊢ ⋃_{t \in F (2^{nd} (x) + 1)} (B (x) \cap (t B (2^{nd} (x) + 1))) = B (x) \cap ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1))$
69		oveq1	$⊢ y = t \to y B n = t B n$
70	69	cbviunv	$⊢ ⋃_{y \in F (n)} (y B n) = ⋃_{t \in F (n)} (t B n)$
71		fveq2	$⊢ n = 2^{nd} (x) + 1 \to F (n) = F (2^{nd} (x) + 1)$
72	71	iuneq1d	$⊢ n = 2^{nd} (x) + 1 \to ⋃_{t \in F (n)} (t B n) = ⋃_{t \in F (2^{nd} (x) + 1)} (t B n)$
73	70 72	syl5eq	$⊢ n = 2^{nd} (x) + 1 \to ⋃_{y \in F (n)} (y B n) = ⋃_{t \in F (2^{nd} (x) + 1)} (t B n)$
74		oveq2	$⊢ n = 2^{nd} (x) + 1 \to t B n = t B (2^{nd} (x) + 1)$
75	74	iuneq2d	$⊢ n = 2^{nd} (x) + 1 \to ⋃_{t \in F (2^{nd} (x) + 1)} (t B n) = ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1))$
76	73 75	eqtrd	$⊢ n = 2^{nd} (x) + 1 \to ⋃_{y \in F (n)} (y B n) = ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1))$
77	76	eqeq2d	$⊢ n = 2^{nd} (x) + 1 \to (X = ⋃_{y \in F (n)} (y B n) \leftrightarrow X = ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1)))$
78	77	rspccva	$⊢ (\forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n) \land 2^{nd} (x) + 1 \in ℕ_{0}) \to X = ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1))$
79	7 64 78	syl2an	$⊢ (φ \land x \in G) \to X = ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1))$
80	79	ineq2d	$⊢ (φ \land x \in G) \to B (x) \cap X = B (x) \cap ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1))$
81	15	fveq2d	$⊢ x \in G \to B (x) = B (⟨1^{st} (x), 2^{nd} (x)⟩)$
82		df-ov	$⊢ 1^{st} (x) B 2^{nd} (x) = B (⟨1^{st} (x), 2^{nd} (x)⟩)$
83	81 82	eqtr4di	$⊢ x \in G \to B (x) = 1^{st} (x) B 2^{nd} (x)$
84	83	adantl	$⊢ (φ \land x \in G) \to B (x) = 1^{st} (x) B 2^{nd} (x)$
85		inss1	$⊢ 𝒫 X \cap Fin \subseteq 𝒫 X$
86		ffvelrn	$⊢ (F : ℕ_{0} ⟶ 𝒫 X \cap Fin \land 2^{nd} (x) \in ℕ_{0}) \to F (2^{nd} (x)) \in (𝒫 X \cap Fin)$
87	6 62 86	syl2an	$⊢ (φ \land x \in G) \to F (2^{nd} (x)) \in (𝒫 X \cap Fin)$
88	85 87	sselid	$⊢ (φ \land x \in G) \to F (2^{nd} (x)) \in 𝒫 X$
89	88	elpwid	$⊢ (φ \land x \in G) \to F (2^{nd} (x)) \subseteq X$
90	23	simp2d	$⊢ x \in G \to 1^{st} (x) \in F (2^{nd} (x))$
91	90	adantl	$⊢ (φ \land x \in G) \to 1^{st} (x) \in F (2^{nd} (x))$
92	89 91	sseldd	$⊢ (φ \land x \in G) \to 1^{st} (x) \in X$
93	62	adantl	$⊢ (φ \land x \in G) \to 2^{nd} (x) \in ℕ_{0}$
94		oveq1	$⊢ z = 1^{st} (x) \to z ball (D) (\frac{1}{2^{m}}) = 1^{st} (x) ball (D) (\frac{1}{2^{m}})$
95		oveq2	$⊢ m = 2^{nd} (x) \to 2^{m} = 2^{2^{nd} (x)}$
96	95	oveq2d	$⊢ m = 2^{nd} (x) \to \frac{1}{2^{m}} = \frac{1}{2^{2^{nd} (x)}}$
97	96	oveq2d	$⊢ m = 2^{nd} (x) \to 1^{st} (x) ball (D) (\frac{1}{2^{m}}) = 1^{st} (x) ball (D) (\frac{1}{2^{2^{nd} (x)}})$
98		ovex	$⊢ 1^{st} (x) ball (D) (\frac{1}{2^{2^{nd} (x)}}) \in V$
99	94 97 4 98	ovmpo	$⊢ (1^{st} (x) \in X \land 2^{nd} (x) \in ℕ_{0}) \to 1^{st} (x) B 2^{nd} (x) = 1^{st} (x) ball (D) (\frac{1}{2^{2^{nd} (x)}})$
100	92 93 99	syl2anc	$⊢ (φ \land x \in G) \to 1^{st} (x) B 2^{nd} (x) = 1^{st} (x) ball (D) (\frac{1}{2^{2^{nd} (x)}})$
101	84 100	eqtrd	$⊢ (φ \land x \in G) \to B (x) = 1^{st} (x) ball (D) (\frac{1}{2^{2^{nd} (x)}})$
102		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
103	5 102	syl	$⊢ φ \to D \in Met (X)$
104		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
105	103 104	syl	$⊢ φ \to D \in ∞Met (X)$
106	105	adantr	$⊢ (φ \land x \in G) \to D \in ∞Met (X)$
107		2nn	$⊢ 2 \in ℕ$
108		nnexpcl	$⊢ (2 \in ℕ \land 2^{nd} (x) \in ℕ_{0}) \to 2^{2^{nd} (x)} \in ℕ$
109	107 93 108	sylancr	$⊢ (φ \land x \in G) \to 2^{2^{nd} (x)} \in ℕ$
110	109	nnrpd	$⊢ (φ \land x \in G) \to 2^{2^{nd} (x)} \in ℝ^{+}$
111	110	rpreccld	$⊢ (φ \land x \in G) \to \frac{1}{2^{2^{nd} (x)}} \in ℝ^{+}$
112	111	rpxrd	$⊢ (φ \land x \in G) \to \frac{1}{2^{2^{nd} (x)}} \in ℝ^{*}$
113		blssm	$⊢ (D \in ∞Met (X) \land 1^{st} (x) \in X \land \frac{1}{2^{2^{nd} (x)}} \in ℝ^{*}) \to 1^{st} (x) ball (D) (\frac{1}{2^{2^{nd} (x)}}) \subseteq X$
114	106 92 112 113	syl3anc	$⊢ (φ \land x \in G) \to 1^{st} (x) ball (D) (\frac{1}{2^{2^{nd} (x)}}) \subseteq X$
115	101 114	eqsstrd	$⊢ (φ \land x \in G) \to B (x) \subseteq X$
116		df-ss	$⊢ B (x) \subseteq X \leftrightarrow B (x) \cap X = B (x)$
117	115 116	sylib	$⊢ (φ \land x \in G) \to B (x) \cap X = B (x)$
118	80 117	eqtr3d	$⊢ (φ \land x \in G) \to B (x) \cap ⋃_{t \in F (2^{nd} (x) + 1)} (t B (2^{nd} (x) + 1)) = B (x)$
119	68 118	syl5eq	$⊢ (φ \land x \in G) \to ⋃_{t \in F (2^{nd} (x) + 1)} (B (x) \cap (t B (2^{nd} (x) + 1))) = B (x)$
120		eqimss2	$⊢ ⋃_{t \in F (2^{nd} (x) + 1)} (B (x) \cap (t B (2^{nd} (x) + 1))) = B (x) \to B (x) \subseteq ⋃_{t \in F (2^{nd} (x) + 1)} (B (x) \cap (t B (2^{nd} (x) + 1)))$
121	119 120	syl	$⊢ (φ \land x \in G) \to B (x) \subseteq ⋃_{t \in F (2^{nd} (x) + 1)} (B (x) \cap (t B (2^{nd} (x) + 1)))$
122	23	simp3d	$⊢ x \in G \to 1^{st} (x) B 2^{nd} (x) \in K$
123	83 122	eqeltrd	$⊢ x \in G \to B (x) \in K$
124	123	adantl	$⊢ (φ \land x \in G) \to B (x) \in K$
125		fvex	$⊢ B (x) \in V$
126	125	inex1	$⊢ B (x) \cap (t B (2^{nd} (x) + 1)) \in V$
127	1 2 126	heiborlem1	$⊢ (F (2^{nd} (x) + 1) \in Fin \land B (x) \subseteq ⋃_{t \in F (2^{nd} (x) + 1)} (B (x) \cap (t B (2^{nd} (x) + 1))) \land B (x) \in K) \to \exists t \in F (2^{nd} (x) + 1) B (x) \cap (t B (2^{nd} (x) + 1)) \in K$
128	67 121 124 127	syl3anc	$⊢ (φ \land x \in G) \to \exists t \in F (2^{nd} (x) + 1) B (x) \cap (t B (2^{nd} (x) + 1)) \in K$
129	85 66	sselid	$⊢ (φ \land x \in G) \to F (2^{nd} (x) + 1) \in 𝒫 X$
130	129	elpwid	$⊢ (φ \land x \in G) \to F (2^{nd} (x) + 1) \subseteq X$
131	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
132	105 131	syl	$⊢ φ \to X = ⋃ J$
133	132	adantr	$⊢ (φ \land x \in G) \to X = ⋃ J$
134	130 133	sseqtrd	$⊢ (φ \land x \in G) \to F (2^{nd} (x) + 1) \subseteq ⋃ J$
135	134	sselda	$⊢ ((φ \land x \in G) \land t \in F (2^{nd} (x) + 1)) \to t \in ⋃ J$
136	135	adantrr	$⊢ ((φ \land x \in G) \land (t \in F (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)) \to t \in ⋃ J$
137	64	adantl	$⊢ (φ \land x \in G) \to 2^{nd} (x) + 1 \in ℕ_{0}$
138		id	$⊢ t \in F (2^{nd} (x) + 1) \to t \in F (2^{nd} (x) + 1)$
139		snfi	$⊢ \{t B (2^{nd} (x) + 1)\} \in Fin$
140		inss2	$⊢ B (x) \cap (t B (2^{nd} (x) + 1)) \subseteq t B (2^{nd} (x) + 1)$
141		ovex	$⊢ t B (2^{nd} (x) + 1) \in V$
142	141	unisn	$⊢ ⋃ \{t B (2^{nd} (x) + 1)\} = t B (2^{nd} (x) + 1)$
143		uniiun	$⊢ ⋃ \{t B (2^{nd} (x) + 1)\} = ⋃_{g \in \{t B (2^{nd} (x) + 1)\}} g$
144	142 143	eqtr3i	$⊢ t B (2^{nd} (x) + 1) = ⋃_{g \in \{t B (2^{nd} (x) + 1)\}} g$
145	140 144	sseqtri	$⊢ B (x) \cap (t B (2^{nd} (x) + 1)) \subseteq ⋃_{g \in \{t B (2^{nd} (x) + 1)\}} g$
146		vex	$⊢ g \in V$
147	1 2 146	heiborlem1	$⊢ (\{t B (2^{nd} (x) + 1)\} \in Fin \land B (x) \cap (t B (2^{nd} (x) + 1)) \subseteq ⋃_{g \in \{t B (2^{nd} (x) + 1)\}} g \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K) \to \exists g \in \{t B (2^{nd} (x) + 1)\} g \in K$
148	139 145 147	mp3an12	$⊢ B (x) \cap (t B (2^{nd} (x) + 1)) \in K \to \exists g \in \{t B (2^{nd} (x) + 1)\} g \in K$
149		eleq1	$⊢ g = t B (2^{nd} (x) + 1) \to (g \in K \leftrightarrow t B (2^{nd} (x) + 1) \in K)$
150	141 149	rexsn	$⊢ \exists g \in \{t B (2^{nd} (x) + 1)\} g \in K \leftrightarrow t B (2^{nd} (x) + 1) \in K$
151	148 150	sylib	$⊢ B (x) \cap (t B (2^{nd} (x) + 1)) \in K \to t B (2^{nd} (x) + 1) \in K$
152		ovex	$⊢ 2^{nd} (x) + 1 \in V$
153	1 2 3 46 152	heiborlem2	$⊢ t G (2^{nd} (x) + 1) \leftrightarrow (2^{nd} (x) + 1 \in ℕ_{0} \land t \in F (2^{nd} (x) + 1) \land t B (2^{nd} (x) + 1) \in K)$
154	153	biimpri	$⊢ (2^{nd} (x) + 1 \in ℕ_{0} \land t \in F (2^{nd} (x) + 1) \land t B (2^{nd} (x) + 1) \in K) \to t G (2^{nd} (x) + 1)$
155	137 138 151 154	syl3an	$⊢ ((φ \land x \in G) \land t \in F (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K) \to t G (2^{nd} (x) + 1)$
156	155	3expb	$⊢ ((φ \land x \in G) \land (t \in F (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)) \to t G (2^{nd} (x) + 1)$
157		simprr	$⊢ ((φ \land x \in G) \land (t \in F (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)) \to B (x) \cap (t B (2^{nd} (x) + 1)) \in K$
158	136 156 157	jca32	$⊢ ((φ \land x \in G) \land (t \in F (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)) \to (t \in ⋃ J \land (t G (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K))$
159	158	ex	$⊢ (φ \land x \in G) \to ((t \in F (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K) \to (t \in ⋃ J \land (t G (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)))$
160	159	reximdv2	$⊢ (φ \land x \in G) \to (\exists t \in F (2^{nd} (x) + 1) B (x) \cap (t B (2^{nd} (x) + 1)) \in K \to \exists t \in ⋃ J (t G (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K))$
161	128 160	mpd	$⊢ (φ \land x \in G) \to \exists t \in ⋃ J (t G (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)$
162	161	ralrimiva	$⊢ φ \to \forall x \in G \exists t \in ⋃ J (t G (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)$
163	1	fvexi	$⊢ J \in V$
164	163	uniex	$⊢ ⋃ J \in V$
165		breq1	$⊢ t = g (x) \to (t G (2^{nd} (x) + 1) \leftrightarrow g (x) G (2^{nd} (x) + 1))$
166		oveq1	$⊢ t = g (x) \to t B (2^{nd} (x) + 1) = g (x) B (2^{nd} (x) + 1)$
167	166	ineq2d	$⊢ t = g (x) \to B (x) \cap (t B (2^{nd} (x) + 1)) = B (x) \cap (g (x) B (2^{nd} (x) + 1))$
168	167	eleq1d	$⊢ t = g (x) \to (B (x) \cap (t B (2^{nd} (x) + 1)) \in K \leftrightarrow B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)$
169	165 168	anbi12d	$⊢ t = g (x) \to ((t G (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K) \leftrightarrow (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))$
170	164 169	axcc4dom	$⊢ (G ≼ ω \land \forall x \in G \exists t \in ⋃ J (t G (2^{nd} (x) + 1) \land B (x) \cap (t B (2^{nd} (x) + 1)) \in K)) \to \exists g (g : G ⟶ ⋃ J \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))$
171	61 162 170	syl2anc	$⊢ φ \to \exists g (g : G ⟶ ⋃ J \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))$
172		exsimpr	$⊢ \exists g (g : G ⟶ ⋃ J \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)) \to \exists g \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)$
173	171 172	syl	$⊢ φ \to \exists g \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)$

Metamath Proof Explorer

Theorem heiborlem3

Proof