poimirlem30

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
	poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
	poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
	poimirlem30.x	$⊢ X = F ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (n)$
	poimirlem30.2	$⊢ φ \to G : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
	poimirlem30.3	$⊢ (φ \land k \in ℕ) \to ran 1^{st} (G (k)) \subseteq (0 ..^k)$
	poimirlem30.4	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists j \in (0 \dots N) 0 r X$
Assertion	poimirlem30	$⊢ φ \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
3		poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
4		poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
5		poimirlem30.x	$⊢ X = F ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (n)$
6		poimirlem30.2	$⊢ φ \to G : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
7		poimirlem30.3	$⊢ (φ \land k \in ℕ) \to ran 1^{st} (G (k)) \subseteq (0 ..^k)$
8		poimirlem30.4	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists j \in (0 \dots N) 0 r X$
9		elfzonn0	$⊢ i \in (0 ..^k) \to i \in ℕ_{0}$
10	9	nn0red	$⊢ i \in (0 ..^k) \to i \in ℝ$
11		nndivre	$⊢ (i \in ℝ \land k \in ℕ) \to \frac{i}{k} \in ℝ$
12	10 11	sylan	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to \frac{i}{k} \in ℝ$
13		elfzole1	$⊢ i \in (0 ..^k) \to 0 \leq i$
14	10 13	jca	$⊢ i \in (0 ..^k) \to (i \in ℝ \land 0 \leq i)$
15		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
16	15	rpregt0d	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
17		divge0	$⊢ ((i \in ℝ \land 0 \leq i) \land (k \in ℝ \land 0 < k)) \to 0 \leq \frac{i}{k}$
18	14 16 17	syl2an	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to 0 \leq \frac{i}{k}$
19		elfzo0le	$⊢ i \in (0 ..^k) \to i \leq k$
20	19	adantr	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to i \leq k$
21	10	adantr	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to i \in ℝ$
22		1red	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to 1 \in ℝ$
23	15	adantl	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to k \in ℝ^{+}$
24	21 22 23	ledivmuld	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to (\frac{i}{k} \leq 1 \leftrightarrow i \leq k \cdot 1)$
25		nncn	$⊢ k \in ℕ \to k \in ℂ$
26	25	mulid1d	$⊢ k \in ℕ \to k \cdot 1 = k$
27	26	breq2d	$⊢ k \in ℕ \to (i \leq k \cdot 1 \leftrightarrow i \leq k)$
28	27	adantl	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to (i \leq k \cdot 1 \leftrightarrow i \leq k)$
29	24 28	bitrd	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to (\frac{i}{k} \leq 1 \leftrightarrow i \leq k)$
30	20 29	mpbird	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to \frac{i}{k} \leq 1$
31		elicc01	$⊢ \frac{i}{k} \in [0, 1] \leftrightarrow (\frac{i}{k} \in ℝ \land 0 \leq \frac{i}{k} \land \frac{i}{k} \leq 1)$
32	12 18 30 31	syl3anbrc	$⊢ (i \in (0 ..^k) \land k \in ℕ) \to \frac{i}{k} \in [0, 1]$
33	32	ancoms	$⊢ (k \in ℕ \land i \in (0 ..^k)) \to \frac{i}{k} \in [0, 1]$
34		elsni	$⊢ j \in \{k\} \to j = k$
35	34	oveq2d	$⊢ j \in \{k\} \to \frac{i}{j} = \frac{i}{k}$
36	35	eleq1d	$⊢ j \in \{k\} \to (\frac{i}{j} \in [0, 1] \leftrightarrow \frac{i}{k} \in [0, 1])$
37	33 36	syl5ibrcom	$⊢ (k \in ℕ \land i \in (0 ..^k)) \to (j \in \{k\} \to \frac{i}{j} \in [0, 1])$
38	37	impr	$⊢ (k \in ℕ \land (i \in (0 ..^k) \land j \in \{k\})) \to \frac{i}{j} \in [0, 1]$
39	38	adantll	$⊢ ((φ \land k \in ℕ) \land (i \in (0 ..^k) \land j \in \{k\})) \to \frac{i}{j} \in [0, 1]$
40	6	ffvelrnda	$⊢ (φ \land k \in ℕ) \to G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
41		xp1st	$⊢ G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (G (k)) \in ({ℕ_{0}}^{(1 \dots N)})$
42		elmapfn	$⊢ 1^{st} (G (k)) \in ({ℕ_{0}}^{(1 \dots N)}) \to 1^{st} (G (k)) Fn (1 \dots N)$
43	40 41 42	3syl	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) Fn (1 \dots N)$
44		df-f	$⊢ 1^{st} (G (k)) : (1 \dots N) ⟶ (0 ..^k) \leftrightarrow (1^{st} (G (k)) Fn (1 \dots N) \land ran 1^{st} (G (k)) \subseteq (0 ..^k))$
45	43 7 44	sylanbrc	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) : (1 \dots N) ⟶ (0 ..^k)$
46		vex	$⊢ k \in V$
47	46	fconst	$⊢ ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
48	47	a1i	$⊢ (φ \land k \in ℕ) \to ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
49		fzfid	$⊢ (φ \land k \in ℕ) \to (1 \dots N) \in Fin$
50		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
51	39 45 48 49 49 50	off	$⊢ (φ \land k \in ℕ) \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
52	2	eleq2i	$⊢ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in I \leftrightarrow 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in ({[0, 1]}^{(1 \dots N)})$
53		ovex	$⊢ [0, 1] \in V$
54		ovex	$⊢ (1 \dots N) \in V$
55	53 54	elmap	$⊢ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in ({[0, 1]}^{(1 \dots N)}) \leftrightarrow (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
56	52 55	bitri	$⊢ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in I \leftrightarrow (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
57	51 56	sylibr	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in I$
58	57	fmpttd	$⊢ φ \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) : ℕ ⟶ I$
59	58	frnd	$⊢ φ \to ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \subseteq I$
60		ominf	$⊢ \neg ω \in Fin$
61		nnenom	$⊢ ℕ \approx ω$
62		enfi	$⊢ ℕ \approx ω \to (ℕ \in Fin \leftrightarrow ω \in Fin)$
63	61 62	ax-mp	$⊢ ℕ \in Fin \leftrightarrow ω \in Fin$
64		iunid	$⊢ ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} \{c\} = ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
65	64	imaeq2i	$⊢ {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} \{c\}] = {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))]$
66		imaiun	$⊢ {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} \{c\}] = ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}]$
67		ovex	$⊢ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in V$
68		eqid	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) = (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
69	67 68	fnmpti	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) Fn ℕ$
70		dffn3	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) Fn ℕ \leftrightarrow (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) : ℕ ⟶ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
71	69 70	mpbi	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) : ℕ ⟶ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
72		fimacnv	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) : ℕ ⟶ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))] = ℕ$
73	71 72	ax-mp	$⊢ {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))] = ℕ$
74	65 66 73	3eqtr3ri	$⊢ ℕ = ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}]$
75	74	eleq1i	$⊢ ℕ \in Fin \leftrightarrow ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
76	63 75	bitr3i	$⊢ ω \in Fin \leftrightarrow ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
77	60 76	mtbi	$⊢ \neg ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
78		ralnex	$⊢ \forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \neg \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
79	78	rexbii	$⊢ \exists i \in ℕ \forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \exists i \in ℕ \neg \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
80		rexnal	$⊢ \exists i \in ℕ \neg \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \neg \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
81	79 80	bitri	$⊢ \exists i \in ℕ \forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \neg \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
82	81	ralbii	$⊢ \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \exists i \in ℕ \forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \neg \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
83		ralnex	$⊢ \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \neg \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \neg \exists c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
84	82 83	bitri	$⊢ \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \exists i \in ℕ \forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \neg \exists c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
85		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
86		elnnuz	$⊢ i \in ℕ \leftrightarrow i \in ℤ_{\geq 1}$
87		fzouzsplit	$⊢ i \in ℤ_{\geq 1} \to ℤ_{\geq 1} = (1 ..^i) \cup ℤ_{\geq i}$
88	86 87	sylbi	$⊢ i \in ℕ \to ℤ_{\geq 1} = (1 ..^i) \cup ℤ_{\geq i}$
89	85 88	syl5eq	$⊢ i \in ℕ \to ℕ = (1 ..^i) \cup ℤ_{\geq i}$
90	89	difeq1d	$⊢ i \in ℕ \to ℕ ∖ (1 ..^i) = ((1 ..^i) \cup ℤ_{\geq i}) ∖ (1 ..^i)$
91		uncom	$⊢ (1 ..^i) \cup ℤ_{\geq i} = ℤ_{\geq i} \cup (1 ..^i)$
92	91	difeq1i	$⊢ ((1 ..^i) \cup ℤ_{\geq i}) ∖ (1 ..^i) = (ℤ_{\geq i} \cup (1 ..^i)) ∖ (1 ..^i)$
93		difun2	$⊢ (ℤ_{\geq i} \cup (1 ..^i)) ∖ (1 ..^i) = ℤ_{\geq i} ∖ (1 ..^i)$
94	92 93	eqtri	$⊢ ((1 ..^i) \cup ℤ_{\geq i}) ∖ (1 ..^i) = ℤ_{\geq i} ∖ (1 ..^i)$
95	90 94	eqtrdi	$⊢ i \in ℕ \to ℕ ∖ (1 ..^i) = ℤ_{\geq i} ∖ (1 ..^i)$
96		difss	$⊢ ℤ_{\geq i} ∖ (1 ..^i) \subseteq ℤ_{\geq i}$
97	95 96	eqsstrdi	$⊢ i \in ℕ \to ℕ ∖ (1 ..^i) \subseteq ℤ_{\geq i}$
98		ssralv	$⊢ ℕ ∖ (1 ..^i) \subseteq ℤ_{\geq i} \to (\forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \forall k \in (ℕ ∖ (1 ..^i)) \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c)$
99	97 98	syl	$⊢ i \in ℕ \to (\forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \forall k \in (ℕ ∖ (1 ..^i)) \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c)$
100		impexp	$⊢ ((k \in ℕ \land \neg k \in (1 ..^i)) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c) \leftrightarrow (k \in ℕ \to (\neg k \in (1 ..^i) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c))$
101		eldif	$⊢ k \in (ℕ ∖ (1 ..^i)) \leftrightarrow (k \in ℕ \land \neg k \in (1 ..^i))$
102	101	imbi1i	$⊢ (k \in (ℕ ∖ (1 ..^i)) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c) \leftrightarrow ((k \in ℕ \land \neg k \in (1 ..^i)) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c)$
103		con34b	$⊢ (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i)) \leftrightarrow (\neg k \in (1 ..^i) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c)$
104	103	imbi2i	$⊢ (k \in ℕ \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i))) \leftrightarrow (k \in ℕ \to (\neg k \in (1 ..^i) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c))$
105	100 102 104	3bitr4i	$⊢ (k \in (ℕ ∖ (1 ..^i)) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c) \leftrightarrow (k \in ℕ \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i)))$
106	105	albii	$⊢ \forall k (k \in (ℕ ∖ (1 ..^i)) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c) \leftrightarrow \forall k (k \in ℕ \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i)))$
107		df-ral	$⊢ \forall k \in (ℕ ∖ (1 ..^i)) \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow \forall k (k \in (ℕ ∖ (1 ..^i)) \to \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c)$
108		vex	$⊢ c \in V$
109	68	mptiniseg	$⊢ c \in V \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] = \{k \in ℕ \| 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c\}$
110	108 109	ax-mp	$⊢ {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] = \{k \in ℕ \| 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c\}$
111	110	sseq1i	$⊢ {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \subseteq (1 ..^i) \leftrightarrow \{k \in ℕ \| 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c\} \subseteq (1 ..^i)$
112		rabss	$⊢ \{k \in ℕ \| 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c\} \subseteq (1 ..^i) \leftrightarrow \forall k \in ℕ (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i))$
113		df-ral	$⊢ \forall k \in ℕ (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i)) \leftrightarrow \forall k (k \in ℕ \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i)))$
114	111 112 113	3bitri	$⊢ {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \subseteq (1 ..^i) \leftrightarrow \forall k (k \in ℕ \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to k \in (1 ..^i)))$
115	106 107 114	3bitr4i	$⊢ \forall k \in (ℕ ∖ (1 ..^i)) \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \leftrightarrow {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \subseteq (1 ..^i)$
116		fzofi	$⊢ (1 ..^i) \in Fin$
117		ssfi	$⊢ ((1 ..^i) \in Fin \land {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \subseteq (1 ..^i)) \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
118	116 117	mpan	$⊢ {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \subseteq (1 ..^i) \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
119	115 118	sylbi	$⊢ \forall k \in (ℕ ∖ (1 ..^i)) \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
120	99 119	syl6	$⊢ i \in ℕ \to (\forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin)$
121	120	rexlimiv	$⊢ \exists i \in ℕ \forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
122	121	ralimi	$⊢ \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \exists i \in ℕ \forall k \in ℤ_{\geq i} \neg 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
123	84 122	sylbir	$⊢ \neg \exists c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
124		iunfi	$⊢ (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \land \forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin) \to ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin$
125	124	ex	$⊢ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to (\forall c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin \to ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin)$
126	123 125	syl5	$⊢ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to (\neg \exists c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to ⋃_{c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))} {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))}^{-1} [\{c\}] \in Fin)$
127	77 126	mt3i	$⊢ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to \exists c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c$
128		ssrexv	$⊢ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \subseteq I \to (\exists c \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c)$
129	59 127 128	syl2im	$⊢ φ \to (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c)$
130		unitssre	$⊢ [0, 1] \subseteq ℝ$
131		elmapi	$⊢ c \in ({[0, 1]}^{(1 \dots N)}) \to c : (1 \dots N) ⟶ [0, 1]$
132	131 2	eleq2s	$⊢ c \in I \to c : (1 \dots N) ⟶ [0, 1]$
133	132	ffvelrnda	$⊢ (c \in I \land m \in (1 \dots N)) \to c (m) \in [0, 1]$
134	130 133	sseldi	$⊢ (c \in I \land m \in (1 \dots N)) \to c (m) \in ℝ$
135		nnrp	$⊢ i \in ℕ \to i \in ℝ^{+}$
136	135	rpreccld	$⊢ i \in ℕ \to \frac{1}{i} \in ℝ^{+}$
137		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
138	137	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
139		blcntr	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land c (m) \in ℝ \land \frac{1}{i} \in ℝ^{+}) \to c (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
140	138 139	mp3an1	$⊢ (c (m) \in ℝ \land \frac{1}{i} \in ℝ^{+}) \to c (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
141	134 136 140	syl2an	$⊢ ((c \in I \land m \in (1 \dots N)) \land i \in ℕ) \to c (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
142	141	an32s	$⊢ ((c \in I \land i \in ℕ) \land m \in (1 \dots N)) \to c (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
143		fveq1	$⊢ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) = c (m)$
144	143	eleq1d	$⊢ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow c (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
145	142 144	syl5ibrcom	$⊢ ((c \in I \land i \in ℕ) \land m \in (1 \dots N)) \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
146	145	ralrimdva	$⊢ (c \in I \land i \in ℕ) \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
147	146	reximdv	$⊢ (c \in I \land i \in ℕ) \to (\exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
148	147	ralimdva	$⊢ c \in I \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
149	148	reximia	$⊢ \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) = c \to \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
150	129 149	syl6	$⊢ φ \to (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
151	54 53	ixpconst	$⊢ ⨉_{n = 1}^{N} [0, 1] = {[0, 1]}^{(1 \dots N)}$
152	2 151	eqtr4i	$⊢ I = ⨉_{n = 1}^{N} [0, 1]$
153	3 152	oveq12i	$⊢ R ↾_{𝑡} I = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) ↾_{𝑡} ⨉_{n = 1}^{N} [0, 1]$
154		fzfid	$⊢ ⊤ \to (1 \dots N) \in Fin$
155		retop	$⊢ topGen (ran (.)) \in Top$
156	155	fconst6	$⊢ ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
157	156	a1i	$⊢ ⊤ \to ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
158	53	a1i	$⊢ (⊤ \land n \in (1 \dots N)) \to [0, 1] \in V$
159	154 157 158	ptrest	$⊢ ⊤ \to \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) ↾_{𝑡} ⨉_{n = 1}^{N} [0, 1] = \prod_{𝑡} ((n \in (1 \dots N) ⟼ ((1 \dots N) \times \{topGen (ran (.))\}) (n) ↾_{𝑡} [0, 1]))$
160	159	mptru	$⊢ \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) ↾_{𝑡} ⨉_{n = 1}^{N} [0, 1] = \prod_{𝑡} ((n \in (1 \dots N) ⟼ ((1 \dots N) \times \{topGen (ran (.))\}) (n) ↾_{𝑡} [0, 1]))$
161		fvex	$⊢ topGen (ran (.)) \in V$
162	161	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{topGen (ran (.))\}) (n) = topGen (ran (.))$
163	162	oveq1d	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{topGen (ran (.))\}) (n) ↾_{𝑡} [0, 1] = topGen (ran (.)) ↾_{𝑡} [0, 1]$
164	163	mpteq2ia	$⊢ (n \in (1 \dots N) ⟼ ((1 \dots N) \times \{topGen (ran (.))\}) (n) ↾_{𝑡} [0, 1]) = (n \in (1 \dots N) ⟼ topGen (ran (.)) ↾_{𝑡} [0, 1])$
165		fconstmpt	$⊢ (1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\} = (n \in (1 \dots N) ⟼ topGen (ran (.)) ↾_{𝑡} [0, 1])$
166	164 165	eqtr4i	$⊢ (n \in (1 \dots N) ⟼ ((1 \dots N) \times \{topGen (ran (.))\}) (n) ↾_{𝑡} [0, 1]) = (1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\}$
167	166	fveq2i	$⊢ \prod_{𝑡} ((n \in (1 \dots N) ⟼ ((1 \dots N) \times \{topGen (ran (.))\}) (n) ↾_{𝑡} [0, 1])) = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\})$
168	153 160 167	3eqtri	$⊢ R ↾_{𝑡} I = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\})$
169		fzfi	$⊢ (1 \dots N) \in Fin$
170		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
171		iicmp	$⊢ II \in Comp$
172	170 171	eqeltrri	$⊢ topGen (ran (.)) ↾_{𝑡} [0, 1] \in Comp$
173	172	fconst6	$⊢ ((1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\}) : (1 \dots N) ⟶ Comp$
174		ptcmpfi	$⊢ ((1 \dots N) \in Fin \land ((1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\}) : (1 \dots N) ⟶ Comp) \to \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\}) \in Comp$
175	169 173 174	mp2an	$⊢ \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.)) ↾_{𝑡} [0, 1]\}) \in Comp$
176	168 175	eqeltri	$⊢ R ↾_{𝑡} I \in Comp$
177		rehaus	$⊢ topGen (ran (.)) \in Haus$
178	177	fconst6	$⊢ ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Haus$
179		pthaus	$⊢ ((1 \dots N) \in Fin \land ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Haus) \to \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) \in Haus$
180	169 178 179	mp2an	$⊢ \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) \in Haus$
181	3 180	eqeltri	$⊢ R \in Haus$
182		haustop	$⊢ R \in Haus \to R \in Top$
183	181 182	ax-mp	$⊢ R \in Top$
184		reex	$⊢ ℝ \in V$
185		mapss	$⊢ (ℝ \in V \land [0, 1] \subseteq ℝ) \to {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
186	184 130 185	mp2an	$⊢ {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
187	2 186	eqsstri	$⊢ I \subseteq ℝ^{(1 \dots N)}$
188		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
189	3 188	ptuniconst	$⊢ ((1 \dots N) \in Fin \land topGen (ran (.)) \in Top) \to ℝ^{(1 \dots N)} = ⋃ R$
190	169 155 189	mp2an	$⊢ ℝ^{(1 \dots N)} = ⋃ R$
191	190	restuni	$⊢ (R \in Top \land I \subseteq ℝ^{(1 \dots N)}) \to I = ⋃ (R ↾_{𝑡} I)$
192	183 187 191	mp2an	$⊢ I = ⋃ (R ↾_{𝑡} I)$
193	192	bwth	$⊢ (R ↾_{𝑡} I \in Comp \land ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \subseteq I \land \neg ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin) \to \exists c \in I c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})))$
194	193	3expia	$⊢ (R ↾_{𝑡} I \in Comp \land ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \subseteq I) \to (\neg ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to \exists c \in I c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))))$
195	176 59 194	sylancr	$⊢ φ \to (\neg ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to \exists c \in I c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))))$
196		cmptop	$⊢ R ↾_{𝑡} I \in Comp \to R ↾_{𝑡} I \in Top$
197	176 196	ax-mp	$⊢ R ↾_{𝑡} I \in Top$
198	192	islp3	$⊢ (R ↾_{𝑡} I \in Top \land ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \subseteq I \land c \in I) \to (c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \leftrightarrow \forall v \in (R ↾_{𝑡} I) (c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset))$
199	197 198	mp3an1	$⊢ (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \subseteq I \land c \in I) \to (c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \leftrightarrow \forall v \in (R ↾_{𝑡} I) (c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset))$
200	59 199	sylan	$⊢ (φ \land c \in I) \to (c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \leftrightarrow \forall v \in (R ↾_{𝑡} I) (c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset))$
201		fzfid	$⊢ (c \in I \land i \in ℕ) \to (1 \dots N) \in Fin$
202	156	a1i	$⊢ (c \in I \land i \in ℕ) \to ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
203		nnrecre	$⊢ i \in ℕ \to \frac{1}{i} \in ℝ$
204	203	rexrd	$⊢ i \in ℕ \to \frac{1}{i} \in ℝ^{*}$
205		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
206	137 205	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
207	206	blopn	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land c (m) \in ℝ \land \frac{1}{i} \in ℝ^{*}) \to c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) \in topGen (ran (.))$
208	138 207	mp3an1	$⊢ (c (m) \in ℝ \land \frac{1}{i} \in ℝ^{*}) \to c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) \in topGen (ran (.))$
209	134 204 208	syl2an	$⊢ ((c \in I \land m \in (1 \dots N)) \land i \in ℕ) \to c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) \in topGen (ran (.))$
210	209	an32s	$⊢ ((c \in I \land i \in ℕ) \land m \in (1 \dots N)) \to c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) \in topGen (ran (.))$
211	161	fvconst2	$⊢ m \in (1 \dots N) \to ((1 \dots N) \times \{topGen (ran (.))\}) (m) = topGen (ran (.))$
212	211	adantl	$⊢ ((c \in I \land i \in ℕ) \land m \in (1 \dots N)) \to ((1 \dots N) \times \{topGen (ran (.))\}) (m) = topGen (ran (.))$
213	210 212	eleqtrrd	$⊢ ((c \in I \land i \in ℕ) \land m \in (1 \dots N)) \to c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) \in ((1 \dots N) \times \{topGen (ran (.))\}) (m)$
214		noel	$⊢ \neg m \in \emptyset$
215		difid	$⊢ (1 \dots N) ∖ (1 \dots N) = \emptyset$
216	215	eleq2i	$⊢ m \in ((1 \dots N) ∖ (1 \dots N)) \leftrightarrow m \in \emptyset$
217	214 216	mtbir	$⊢ \neg m \in ((1 \dots N) ∖ (1 \dots N))$
218	217	pm2.21i	$⊢ m \in ((1 \dots N) ∖ (1 \dots N)) \to c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (m)$
219	218	adantl	$⊢ ((c \in I \land i \in ℕ) \land m \in ((1 \dots N) ∖ (1 \dots N))) \to c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (m)$
220	201 202 201 213 219	ptopn	$⊢ (c \in I \land i \in ℕ) \to ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \in \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
221	220 3	eleqtrrdi	$⊢ (c \in I \land i \in ℕ) \to ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \in R$
222		ovex	$⊢ {[0, 1]}^{(1 \dots N)} \in V$
223	2 222	eqeltri	$⊢ I \in V$
224		elrestr	$⊢ (R \in Haus \land I \in V \land ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \in R) \to ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I \in (R ↾_{𝑡} I)$
225	181 223 224	mp3an12	$⊢ ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \in R \to ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I \in (R ↾_{𝑡} I)$
226	221 225	syl	$⊢ (c \in I \land i \in ℕ) \to ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I \in (R ↾_{𝑡} I)$
227		difss	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \subseteq (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]$
228		imassrn	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \subseteq ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
229	227 228	sstri	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \subseteq ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
230	229 59	sstrid	$⊢ φ \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \subseteq I$
231		haust1	$⊢ R \in Haus \to R \in Fre$
232	181 231	ax-mp	$⊢ R \in Fre$
233		restt1	$⊢ (R \in Fre \land I \in V) \to R ↾_{𝑡} I \in Fre$
234	232 223 233	mp2an	$⊢ R ↾_{𝑡} I \in Fre$
235		funmpt	$⊢ Fun (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
236		imafi	$⊢ (Fun (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land (1 ..^i) \in Fin) \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \in Fin$
237	235 116 236	mp2an	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \in Fin$
238		diffi	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \in Fin \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \in Fin$
239	237 238	ax-mp	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \in Fin$
240	192	t1ficld	$⊢ (R ↾_{𝑡} I \in Fre \land (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \subseteq I \land (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \in Fin) \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \in Clsd (R ↾_{𝑡} I)$
241	234 239 240	mp3an13	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \subseteq I \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \in Clsd (R ↾_{𝑡} I)$
242	230 241	syl	$⊢ φ \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \in Clsd (R ↾_{𝑡} I)$
243	192	difopn	$⊢ (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I \in (R ↾_{𝑡} I) \land (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\} \in Clsd (R ↾_{𝑡} I)) \to (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \in (R ↾_{𝑡} I)$
244	226 242 243	syl2anr	$⊢ (φ \land (c \in I \land i \in ℕ)) \to (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \in (R ↾_{𝑡} I)$
245	244	anassrs	$⊢ ((φ \land c \in I) \land i \in ℕ) \to (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \in (R ↾_{𝑡} I)$
246		eleq2	$⊢ v = (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \to (c \in v \leftrightarrow c \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})))$
247		ineq1	$⊢ v = (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) = ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})$
248	247	neeq1d	$⊢ v = (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \to (v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset \leftrightarrow ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset)$
249	246 248	imbi12d	$⊢ v = (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \to ((c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset) \leftrightarrow (c \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \to ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset))$
250	249	rspcva	$⊢ ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \in (R ↾_{𝑡} I) \land \forall v \in (R ↾_{𝑡} I) (c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset)) \to (c \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \to ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset)$
251	132	ffnd	$⊢ c \in I \to c Fn (1 \dots N)$
252	251	adantr	$⊢ (c \in I \land i \in ℕ) \to c Fn (1 \dots N)$
253	142	ralrimiva	$⊢ (c \in I \land i \in ℕ) \to \forall m \in (1 \dots N) c (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
254	108	elixp	$⊢ c \in ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow (c Fn (1 \dots N) \land \forall m \in (1 \dots N) c (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
255	252 253 254	sylanbrc	$⊢ (c \in I \land i \in ℕ) \to c \in ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
256		simpl	$⊢ (c \in I \land i \in ℕ) \to c \in I$
257	255 256	elind	$⊢ (c \in I \land i \in ℕ) \to c \in (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I)$
258		neldifsnd	$⊢ (c \in I \land i \in ℕ) \to \neg c \in ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})$
259	257 258	eldifd	$⊢ (c \in I \land i \in ℕ) \to c \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}))$
260	259	adantll	$⊢ ((φ \land c \in I) \land i \in ℕ) \to c \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}))$
261		simplr	$⊢ ((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \to \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
262	261	anim1i	$⊢ (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \to (\forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)])$
263		simpl	$⊢ (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\}) \to j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
264	262 263	anim12i	$⊢ ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})) \to ((\forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})))$
265		elin	$⊢ j \in (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})) \leftrightarrow (j \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \land j \in (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}))$
266		andir	$⊢ (((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \lor (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\})) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})) \leftrightarrow (((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})) \lor ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\}) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})))$
267		eldif	$⊢ j \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \leftrightarrow (j \in (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) \land \neg j \in ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}))$
268		elin	$⊢ j \in (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) \leftrightarrow (j \in ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land j \in I)$
269		vex	$⊢ j \in V$
270	269	elixp	$⊢ j \in ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow (j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
271	270	anbi1i	$⊢ (j \in ⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land j \in I) \leftrightarrow ((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I)$
272	268 271	bitri	$⊢ j \in (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) \leftrightarrow ((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I)$
273		ianor	$⊢ \neg (j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land \neg j \in \{c\}) \leftrightarrow (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \lor \neg \neg j \in \{c\})$
274		eldif	$⊢ j \in ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \leftrightarrow (j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land \neg j \in \{c\})$
275	273 274	xchnxbir	$⊢ \neg j \in ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \leftrightarrow (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \lor \neg \neg j \in \{c\})$
276	272 275	anbi12i	$⊢ (j \in (⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) \land \neg j \in ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \leftrightarrow (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \lor \neg \neg j \in \{c\}))$
277		andi	$⊢ (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \lor \neg \neg j \in \{c\})) \leftrightarrow ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \lor (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\}))$
278	267 276 277	3bitri	$⊢ j \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \leftrightarrow ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \lor (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\}))$
279		eldif	$⊢ j \in (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \leftrightarrow (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})$
280	278 279	anbi12i	$⊢ (j \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \land j \in (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})) \leftrightarrow (((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \lor (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\})) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\}))$
281		pm3.24	$⊢ \neg (\neg j \in \{c\} \land \neg \neg j \in \{c\})$
282		simpr	$⊢ (((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\}) \to \neg \neg j \in \{c\}$
283		simpr	$⊢ (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\}) \to \neg j \in \{c\}$
284	282 283	anim12ci	$⊢ ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\}) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})) \to (\neg j \in \{c\} \land \neg \neg j \in \{c\})$
285	281 284	mto	$⊢ \neg ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\}) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\}))$
286	285	biorfi	$⊢ ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})) \leftrightarrow (((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})) \lor ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg \neg j \in \{c\}) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\})))$
287	266 280 286	3bitr4i	$⊢ (j \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \land j \in (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})) \leftrightarrow ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\}))$
288	265 287	bitri	$⊢ j \in (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})) \leftrightarrow ((((j Fn (1 \dots N) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \land j \in I) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in \{c\}))$
289		ancom	$⊢ ((\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \leftrightarrow (\forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))))$
290		anass	$⊢ ((\forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \leftrightarrow (\forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))))$
291	289 290	bitr4i	$⊢ ((\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \leftrightarrow ((\forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})))$
292	264 288 291	3imtr4i	$⊢ j \in (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})) \to ((\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
293		ancom	$⊢ (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \leftrightarrow (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)])$
294		eldif	$⊢ j \in (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \leftrightarrow (j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)])$
295	293 294	bitr4i	$⊢ (\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \leftrightarrow j \in (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)])$
296		imadmrn	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [dom (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))] = ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
297	67 68	dmmpti	$⊢ dom (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) = ℕ$
298	297	imaeq2i	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [dom (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))] = (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ]$
299	296 298	eqtr3i	$⊢ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) = (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ]$
300	299	difeq1i	$⊢ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] = (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ] ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]$
301		imadifss	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ] ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \subseteq (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ ∖ (1 ..^i)]$
302	300 301	eqsstri	$⊢ ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \subseteq (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ ∖ (1 ..^i)]$
303		imass2	$⊢ ℕ ∖ (1 ..^i) \subseteq ℤ_{\geq i} \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ ∖ (1 ..^i)] \subseteq (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℤ_{\geq i}]$
304	97 303	syl	$⊢ i \in ℕ \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ ∖ (1 ..^i)] \subseteq (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℤ_{\geq i}]$
305		df-ima	$⊢ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℤ_{\geq i}] = ran ({(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ↾}_{ℤ_{\geq i}})$
306		uznnssnn	$⊢ i \in ℕ \to ℤ_{\geq i} \subseteq ℕ$
307	306	resmptd	$⊢ i \in ℕ \to {(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ↾}_{ℤ_{\geq i}} = (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
308	307	rneqd	$⊢ i \in ℕ \to ran ({(k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ↾}_{ℤ_{\geq i}}) = ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
309	305 308	syl5eq	$⊢ i \in ℕ \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℤ_{\geq i}] = ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
310	304 309	sseqtrd	$⊢ i \in ℕ \to (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [ℕ ∖ (1 ..^i)] \subseteq ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
311	302 310	sstrid	$⊢ i \in ℕ \to ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \subseteq ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
312	311	sseld	$⊢ i \in ℕ \to (j \in (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)]) \to j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})))$
313	295 312	syl5bi	$⊢ i \in ℕ \to ((\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \to j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})))$
314	313	anim1d	$⊢ i \in ℕ \to (((\neg j \in (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] \land j \in ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))) \to (j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))))$
315	292 314	syl5	$⊢ i \in ℕ \to (j \in (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})) \to (j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))))$
316	315	eximdv	$⊢ i \in ℕ \to (\exists j j \in (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\})) \to \exists j (j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))))$
317		n0	$⊢ ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset \leftrightarrow \exists j j \in (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}))$
318	67	rgenw	$⊢ \forall k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in V$
319		eqid	$⊢ (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) = (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))$
320		fveq1	$⊢ j = 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \to j (m) = (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m)$
321	320	eleq1d	$⊢ j = 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \to (j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
322	321	ralbidv	$⊢ j = 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \to (\forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
323	319 322	rexrnmptw	$⊢ \forall k \in ℤ_{\geq i} 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}) \in V \to (\exists j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
324	318 323	ax-mp	$⊢ \exists j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
325		df-rex	$⊢ \exists j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow \exists j (j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
326	324 325	bitr3i	$⊢ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow \exists j (j \in ran (k \in ℤ_{\geq i} ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \land \forall m \in (1 \dots N) j (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
327	316 317 326	3imtr4g	$⊢ i \in ℕ \to (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset \to \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
328	327	adantl	$⊢ ((φ \land c \in I) \land i \in ℕ) \to (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset \to \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
329	260 328	embantd	$⊢ ((φ \land c \in I) \land i \in ℕ) \to ((c \in ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \to ((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\})) \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset) \to \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
330	250 329	syl5	$⊢ ((φ \land c \in I) \land i \in ℕ) \to (((⨉_{m = 1}^{N} (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \cap I) ∖ ((k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) [(1 ..^i)] ∖ \{c\}) \in (R ↾_{𝑡} I) \land \forall v \in (R ↾_{𝑡} I) (c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset)) \to \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
331	245 330	mpand	$⊢ ((φ \land c \in I) \land i \in ℕ) \to (\forall v \in (R ↾_{𝑡} I) (c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset) \to \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
332	331	ralrimdva	$⊢ (φ \land c \in I) \to (\forall v \in (R ↾_{𝑡} I) (c \in v \to v \cap (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) ∖ \{c\}) \neq \emptyset) \to \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
333	200 332	sylbid	$⊢ (φ \land c \in I) \to (c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \to \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
334	333	reximdva	$⊢ φ \to (\exists c \in I c \in limPt (R ↾_{𝑡} I) (ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\}))) \to \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
335	195 334	syld	$⊢ φ \to (\neg ran (k \in ℕ ⟼ 1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) \in Fin \to \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})))$
336	150 335	pm2.61d	$⊢ φ \to \exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}))$
337	1 2 3 4 5 6 7 8	poimirlem29	$⊢ φ \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
338	337	reximdv	$⊢ φ \to (\exists c \in I \forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (c (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
339	336 338	mpd	$⊢ φ \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$

Metamath Proof Explorer

Theorem poimirlem30

Proof