heiborlem4

Description: Lemma for heibor . Using the function T constructed in heiborlem3 , construct an infinite path in G . (Contributed by Jeff Madsen, 23-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)$
	heibor.9	$⊢ φ \to \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K)$
	heibor.10	$⊢ φ \to C G 0$
	heibor.11	$⊢ S = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)))$
Assertion	heiborlem4	$⊢ (φ \land A \in ℕ_{0}) \to S (A) G A$

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		heibor.9	$⊢ φ \to \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K)$
9		heibor.10	$⊢ φ \to C G 0$
10		heibor.11	$⊢ S = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)))$
11		fveq2	$⊢ x = 0 \to S (x) = S (0)$
12		id	$⊢ x = 0 \to x = 0$
13	11 12	breq12d	$⊢ x = 0 \to (S (x) G x \leftrightarrow S (0) G 0)$
14	13	imbi2d	$⊢ x = 0 \to ((φ \to S (x) G x) \leftrightarrow (φ \to S (0) G 0))$
15		fveq2	$⊢ x = k \to S (x) = S (k)$
16		id	$⊢ x = k \to x = k$
17	15 16	breq12d	$⊢ x = k \to (S (x) G x \leftrightarrow S (k) G k)$
18	17	imbi2d	$⊢ x = k \to ((φ \to S (x) G x) \leftrightarrow (φ \to S (k) G k))$
19		fveq2	$⊢ x = k + 1 \to S (x) = S (k + 1)$
20		id	$⊢ x = k + 1 \to x = k + 1$
21	19 20	breq12d	$⊢ x = k + 1 \to (S (x) G x \leftrightarrow S (k + 1) G (k + 1))$
22	21	imbi2d	$⊢ x = k + 1 \to ((φ \to S (x) G x) \leftrightarrow (φ \to S (k + 1) G (k + 1)))$
23		fveq2	$⊢ x = A \to S (x) = S (A)$
24		id	$⊢ x = A \to x = A$
25	23 24	breq12d	$⊢ x = A \to (S (x) G x \leftrightarrow S (A) G A)$
26	25	imbi2d	$⊢ x = A \to ((φ \to S (x) G x) \leftrightarrow (φ \to S (A) G A))$
27	10	fveq1i	$⊢ S (0) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (0)$
28		0z	$⊢ 0 \in ℤ$
29		seq1	$⊢ 0 \in ℤ \to seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (0) = (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (0)$
30	28 29	ax-mp	$⊢ seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (0) = (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (0)$
31	27 30	eqtri	$⊢ S (0) = (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (0)$
32		0nn0	$⊢ 0 \in ℕ_{0}$
33	3	relopabiv	$⊢ Rel G$
34	33	brrelex1i	$⊢ C G 0 \to C \in V$
35	9 34	syl	$⊢ φ \to C \in V$
36		iftrue	$⊢ m = 0 \to if (m = 0, C, m - 1) = C$
37		eqid	$⊢ (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) = (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))$
38	36 37	fvmptg	$⊢ (0 \in ℕ_{0} \land C \in V) \to (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (0) = C$
39	32 35 38	sylancr	$⊢ φ \to (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (0) = C$
40	31 39	eqtrid	$⊢ φ \to S (0) = C$
41	40 9	eqbrtrd	$⊢ φ \to S (0) G 0$
42		df-br	$⊢ S (k) G k \leftrightarrow ⟨S (k), k⟩ \in G$
43		fveq2	$⊢ x = ⟨S (k), k⟩ \to T (x) = T (⟨S (k), k⟩)$
44		df-ov	$⊢ S (k) T k = T (⟨S (k), k⟩)$
45	43 44	eqtr4di	$⊢ x = ⟨S (k), k⟩ \to T (x) = S (k) T k$
46		fvex	$⊢ S (k) \in V$
47		vex	$⊢ k \in V$
48	46 47	op2ndd	$⊢ x = ⟨S (k), k⟩ \to 2^{nd} (x) = k$
49	48	oveq1d	$⊢ x = ⟨S (k), k⟩ \to 2^{nd} (x) + 1 = k + 1$
50	45 49	breq12d	$⊢ x = ⟨S (k), k⟩ \to (T (x) G (2^{nd} (x) + 1) \leftrightarrow (S (k) T k) G (k + 1))$
51		fveq2	$⊢ x = ⟨S (k), k⟩ \to B (x) = B (⟨S (k), k⟩)$
52		df-ov	$⊢ S (k) B k = B (⟨S (k), k⟩)$
53	51 52	eqtr4di	$⊢ x = ⟨S (k), k⟩ \to B (x) = S (k) B k$
54	45 49	oveq12d	$⊢ x = ⟨S (k), k⟩ \to T (x) B (2^{nd} (x) + 1) = (S (k) T k) B (k + 1)$
55	53 54	ineq12d	$⊢ x = ⟨S (k), k⟩ \to B (x) \cap (T (x) B (2^{nd} (x) + 1)) = (S (k) B k) \cap ((S (k) T k) B (k + 1))$
56	55	eleq1d	$⊢ x = ⟨S (k), k⟩ \to (B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K \leftrightarrow (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K)$
57	50 56	anbi12d	$⊢ x = ⟨S (k), k⟩ \to ((T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K) \leftrightarrow ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
58	57	rspccv	$⊢ \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K) \to (⟨S (k), k⟩ \in G \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
59	8 58	syl	$⊢ φ \to (⟨S (k), k⟩ \in G \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
60	42 59	biimtrid	$⊢ φ \to (S (k) G k \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
61		seqp1	$⊢ k \in ℤ_{\geq 0} \to seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
62		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
63	61 62	eleq2s	$⊢ k \in ℕ_{0} \to seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
64	10	fveq1i	$⊢ S (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k + 1)$
65	10	fveq1i	$⊢ S (k) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k)$
66	65	oveq1i	$⊢ S (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
67	63 64 66	3eqtr4g	$⊢ k \in ℕ_{0} \to S (k + 1) = S (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
68		eqeq1	$⊢ m = k + 1 \to (m = 0 \leftrightarrow k + 1 = 0)$
69		oveq1	$⊢ m = k + 1 \to m - 1 = k + 1 - 1$
70	68 69	ifbieq2d	$⊢ m = k + 1 \to if (m = 0, C, m - 1) = if (k + 1 = 0, C, k + 1 - 1)$
71		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
72		nn0p1nn	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ$
73		nnne0	$⊢ k + 1 \in ℕ \to k + 1 \neq 0$
74	73	neneqd	$⊢ k + 1 \in ℕ \to \neg k + 1 = 0$
75		iffalse	$⊢ \neg k + 1 = 0 \to if (k + 1 = 0, C, k + 1 - 1) = k + 1 - 1$
76	72 74 75	3syl	$⊢ k \in ℕ_{0} \to if (k + 1 = 0, C, k + 1 - 1) = k + 1 - 1$
77		ovex	$⊢ k + 1 - 1 \in V$
78	76 77	eqeltrdi	$⊢ k \in ℕ_{0} \to if (k + 1 = 0, C, k + 1 - 1) \in V$
79	37 70 71 78	fvmptd3	$⊢ k \in ℕ_{0} \to (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = if (k + 1 = 0, C, k + 1 - 1)$
80		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
81		ax-1cn	$⊢ 1 \in ℂ$
82		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
83	80 81 82	sylancl	$⊢ k \in ℕ_{0} \to k + 1 - 1 = k$
84	79 76 83	3eqtrd	$⊢ k \in ℕ_{0} \to (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = k$
85	84	oveq2d	$⊢ k \in ℕ_{0} \to S (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = S (k) T k$
86	67 85	eqtrd	$⊢ k \in ℕ_{0} \to S (k + 1) = S (k) T k$
87	86	breq1d	$⊢ k \in ℕ_{0} \to (S (k + 1) G (k + 1) \leftrightarrow (S (k) T k) G (k + 1))$
88	87	biimprd	$⊢ k \in ℕ_{0} \to ((S (k) T k) G (k + 1) \to S (k + 1) G (k + 1))$
89	88	adantrd	$⊢ k \in ℕ_{0} \to (((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K) \to S (k + 1) G (k + 1))$
90	60 89	syl9r	$⊢ k \in ℕ_{0} \to (φ \to (S (k) G k \to S (k + 1) G (k + 1)))$
91	90	a2d	$⊢ k \in ℕ_{0} \to ((φ \to S (k) G k) \to (φ \to S (k + 1) G (k + 1)))$
92	14 18 22 26 41 91	nn0ind	$⊢ A \in ℕ_{0} \to (φ \to S (A) G A)$
93	92	impcom	$⊢ (φ \land A \in ℕ_{0}) \to S (A) G A$

Metamath Proof Explorer

Theorem heiborlem4

Proof