1stckgenlem

Description: The one-point compactification of NN is compact. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Hypotheses	1stckgen.1	$⊢ φ \to J \in TopOn (X)$
	1stckgen.2	$⊢ φ \to F : ℕ ⟶ X$
	1stckgen.3	$⊢ φ \to F \underset{t}{⇝} (J) A$
Assertion	1stckgenlem	$⊢ φ \to J ↾_{𝑡} (ran F \cup \{A\}) \in Comp$

Proof

Step	Hyp	Ref	Expression
1		1stckgen.1	$⊢ φ \to J \in TopOn (X)$
2		1stckgen.2	$⊢ φ \to F : ℕ ⟶ X$
3		1stckgen.3	$⊢ φ \to F \underset{t}{⇝} (J) A$
4		simprr	$⊢ (φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \to ran F \cup \{A\} \subseteq ⋃ u$
5		ssun2	$⊢ \{A\} \subseteq ran F \cup \{A\}$
6		lmcl	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) A) \to A \in X$
7	1 3 6	syl2anc	$⊢ φ \to A \in X$
8		snssg	$⊢ A \in X \to (A \in (ran F \cup \{A\}) \leftrightarrow \{A\} \subseteq ran F \cup \{A\})$
9	7 8	syl	$⊢ φ \to (A \in (ran F \cup \{A\}) \leftrightarrow \{A\} \subseteq ran F \cup \{A\})$
10	5 9	mpbiri	$⊢ φ \to A \in (ran F \cup \{A\})$
11	10	adantr	$⊢ (φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \to A \in (ran F \cup \{A\})$
12	4 11	sseldd	$⊢ (φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \to A \in ⋃ u$
13		eluni2	$⊢ A \in ⋃ u \leftrightarrow \exists w \in u A \in w$
14	12 13	sylib	$⊢ (φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \to \exists w \in u A \in w$
15		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
16		simprr	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to A \in w$
17		1zzd	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to 1 \in ℤ$
18	3	ad2antrr	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to F \underset{t}{⇝} (J) A$
19		simplrl	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to u \in 𝒫 J$
20	19	elpwid	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to u \subseteq J$
21		simprl	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to w \in u$
22	20 21	sseldd	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to w \in J$
23	15 16 17 18 22	lmcvg	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in w$
24		imassrn	$⊢ F [(1 \dots j)] \subseteq ran F$
25		ssun1	$⊢ ran F \subseteq ran F \cup \{A\}$
26	24 25	sstri	$⊢ F [(1 \dots j)] \subseteq ran F \cup \{A\}$
27		id	$⊢ ran F \cup \{A\} \subseteq ⋃ u \to ran F \cup \{A\} \subseteq ⋃ u$
28	26 27	sstrid	$⊢ ran F \cup \{A\} \subseteq ⋃ u \to F [(1 \dots j)] \subseteq ⋃ u$
29	2	frnd	$⊢ φ \to ran F \subseteq X$
30	24 29	sstrid	$⊢ φ \to F [(1 \dots j)] \subseteq X$
31		resttopon	$⊢ (J \in TopOn (X) \land F [(1 \dots j)] \subseteq X) \to J ↾_{𝑡} F [(1 \dots j)] \in TopOn (F [(1 \dots j)])$
32	1 30 31	syl2anc	$⊢ φ \to J ↾_{𝑡} F [(1 \dots j)] \in TopOn (F [(1 \dots j)])$
33		topontop	$⊢ J ↾_{𝑡} F [(1 \dots j)] \in TopOn (F [(1 \dots j)]) \to J ↾_{𝑡} F [(1 \dots j)] \in Top$
34	32 33	syl	$⊢ φ \to J ↾_{𝑡} F [(1 \dots j)] \in Top$
35		fzfid	$⊢ φ \to (1 \dots j) \in Fin$
36	2	ffund	$⊢ φ \to Fun F$
37		fz1ssnn	$⊢ (1 \dots j) \subseteq ℕ$
38	2	fdmd	$⊢ φ \to dom F = ℕ$
39	37 38	sseqtrrid	$⊢ φ \to (1 \dots j) \subseteq dom F$
40		fores	$⊢ (Fun F \land (1 \dots j) \subseteq dom F) \to ({F ↾}_{(1 \dots j)}) : (1 \dots j) \underset{onto}{⟶} F [(1 \dots j)]$
41	36 39 40	syl2anc	$⊢ φ \to ({F ↾}_{(1 \dots j)}) : (1 \dots j) \underset{onto}{⟶} F [(1 \dots j)]$
42		fofi	$⊢ ((1 \dots j) \in Fin \land ({F ↾}_{(1 \dots j)}) : (1 \dots j) \underset{onto}{⟶} F [(1 \dots j)]) \to F [(1 \dots j)] \in Fin$
43	35 41 42	syl2anc	$⊢ φ \to F [(1 \dots j)] \in Fin$
44		pwfi	$⊢ F [(1 \dots j)] \in Fin \leftrightarrow 𝒫 F [(1 \dots j)] \in Fin$
45	43 44	sylib	$⊢ φ \to 𝒫 F [(1 \dots j)] \in Fin$
46		restsspw	$⊢ J ↾_{𝑡} F [(1 \dots j)] \subseteq 𝒫 F [(1 \dots j)]$
47		ssfi	$⊢ (𝒫 F [(1 \dots j)] \in Fin \land J ↾_{𝑡} F [(1 \dots j)] \subseteq 𝒫 F [(1 \dots j)]) \to J ↾_{𝑡} F [(1 \dots j)] \in Fin$
48	45 46 47	sylancl	$⊢ φ \to J ↾_{𝑡} F [(1 \dots j)] \in Fin$
49	34 48	elind	$⊢ φ \to J ↾_{𝑡} F [(1 \dots j)] \in (Top \cap Fin)$
50		fincmp	$⊢ J ↾_{𝑡} F [(1 \dots j)] \in (Top \cap Fin) \to J ↾_{𝑡} F [(1 \dots j)] \in Comp$
51	49 50	syl	$⊢ φ \to J ↾_{𝑡} F [(1 \dots j)] \in Comp$
52		topontop	$⊢ J \in TopOn (X) \to J \in Top$
53	1 52	syl	$⊢ φ \to J \in Top$
54		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
55	1 54	syl	$⊢ φ \to X = ⋃ J$
56	30 55	sseqtrd	$⊢ φ \to F [(1 \dots j)] \subseteq ⋃ J$
57		eqid	$⊢ ⋃ J = ⋃ J$
58	57	cmpsub	$⊢ (J \in Top \land F [(1 \dots j)] \subseteq ⋃ J) \to (J ↾_{𝑡} F [(1 \dots j)] \in Comp \leftrightarrow \forall u \in 𝒫 J (F [(1 \dots j)] \subseteq ⋃ u \to \exists s \in (𝒫 u \cap Fin) F [(1 \dots j)] \subseteq ⋃ s))$
59	53 56 58	syl2anc	$⊢ φ \to (J ↾_{𝑡} F [(1 \dots j)] \in Comp \leftrightarrow \forall u \in 𝒫 J (F [(1 \dots j)] \subseteq ⋃ u \to \exists s \in (𝒫 u \cap Fin) F [(1 \dots j)] \subseteq ⋃ s))$
60	51 59	mpbid	$⊢ φ \to \forall u \in 𝒫 J (F [(1 \dots j)] \subseteq ⋃ u \to \exists s \in (𝒫 u \cap Fin) F [(1 \dots j)] \subseteq ⋃ s)$
61	60	r19.21bi	$⊢ (φ \land u \in 𝒫 J) \to (F [(1 \dots j)] \subseteq ⋃ u \to \exists s \in (𝒫 u \cap Fin) F [(1 \dots j)] \subseteq ⋃ s)$
62	28 61	syl5	$⊢ (φ \land u \in 𝒫 J) \to (ran F \cup \{A\} \subseteq ⋃ u \to \exists s \in (𝒫 u \cap Fin) F [(1 \dots j)] \subseteq ⋃ s)$
63	62	impr	$⊢ (φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \to \exists s \in (𝒫 u \cap Fin) F [(1 \dots j)] \subseteq ⋃ s$
64	63	adantr	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \to \exists s \in (𝒫 u \cap Fin) F [(1 \dots j)] \subseteq ⋃ s$
65		simprl	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \in (𝒫 u \cap Fin)$
66	65	elin1d	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \in 𝒫 u$
67	66	elpwid	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \subseteq u$
68		simprll	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \to w \in u$
69	68	adantr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to w \in u$
70	69	snssd	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to \{w\} \subseteq u$
71	67 70	unssd	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \cup \{w\} \subseteq u$
72		vex	$⊢ u \in V$
73	72	elpw2	$⊢ s \cup \{w\} \in 𝒫 u \leftrightarrow s \cup \{w\} \subseteq u$
74	71 73	sylibr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \cup \{w\} \in 𝒫 u$
75	65	elin2d	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \in Fin$
76		snfi	$⊢ \{w\} \in Fin$
77		unfi	$⊢ (s \in Fin \land \{w\} \in Fin) \to s \cup \{w\} \in Fin$
78	75 76 77	sylancl	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \cup \{w\} \in Fin$
79	74 78	elind	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to s \cup \{w\} \in (𝒫 u \cap Fin)$
80	2	ffnd	$⊢ φ \to F Fn ℕ$
81	80	ad3antrrr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to F Fn ℕ$
82		simprrr	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \to \forall k \in ℤ_{\geq j} F (k) \in w$
83	82	adantr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to \forall k \in ℤ_{\geq j} F (k) \in w$
84		fveq2	$⊢ k = n \to F (k) = F (n)$
85	84	eleq1d	$⊢ k = n \to (F (k) \in w \leftrightarrow F (n) \in w)$
86	85	rspccva	$⊢ (\forall k \in ℤ_{\geq j} F (k) \in w \land n \in ℤ_{\geq j}) \to F (n) \in w$
87	83 86	sylan	$⊢ ((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in ℤ_{\geq j}) \to F (n) \in w$
88		elun2	$⊢ F (n) \in w \to F (n) \in (⋃ s \cup w)$
89	87 88	syl	$⊢ ((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in ℤ_{\geq j}) \to F (n) \in (⋃ s \cup w)$
90	89	adantlr	$⊢ (((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in ℕ) \land n \in ℤ_{\geq j}) \to F (n) \in (⋃ s \cup w)$
91		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
92	91	anbi1i	$⊢ (n \in ℕ \land j \in ℤ_{\geq n}) \leftrightarrow (n \in ℤ_{\geq 1} \land j \in ℤ_{\geq n})$
93		elfzuzb	$⊢ n \in (1 \dots j) \leftrightarrow (n \in ℤ_{\geq 1} \land j \in ℤ_{\geq n})$
94	92 93	bitr4i	$⊢ (n \in ℕ \land j \in ℤ_{\geq n}) \leftrightarrow n \in (1 \dots j)$
95		simprr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to F [(1 \dots j)] \subseteq ⋃ s$
96		funimass4	$⊢ (Fun F \land (1 \dots j) \subseteq dom F) \to (F [(1 \dots j)] \subseteq ⋃ s \leftrightarrow \forall n \in (1 \dots j) F (n) \in ⋃ s)$
97	36 39 96	syl2anc	$⊢ φ \to (F [(1 \dots j)] \subseteq ⋃ s \leftrightarrow \forall n \in (1 \dots j) F (n) \in ⋃ s)$
98	97	ad3antrrr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to (F [(1 \dots j)] \subseteq ⋃ s \leftrightarrow \forall n \in (1 \dots j) F (n) \in ⋃ s)$
99	95 98	mpbid	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to \forall n \in (1 \dots j) F (n) \in ⋃ s$
100	99	r19.21bi	$⊢ ((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in (1 \dots j)) \to F (n) \in ⋃ s$
101		elun1	$⊢ F (n) \in ⋃ s \to F (n) \in (⋃ s \cup w)$
102	100 101	syl	$⊢ ((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in (1 \dots j)) \to F (n) \in (⋃ s \cup w)$
103	94 102	sylan2b	$⊢ ((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land (n \in ℕ \land j \in ℤ_{\geq n})) \to F (n) \in (⋃ s \cup w)$
104	103	anassrs	$⊢ (((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in ℕ) \land j \in ℤ_{\geq n}) \to F (n) \in (⋃ s \cup w)$
105		simprl	$⊢ ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w)) \to j \in ℕ$
106	105	ad2antlr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to j \in ℕ$
107		nnz	$⊢ j \in ℕ \to j \in ℤ$
108		nnz	$⊢ n \in ℕ \to n \in ℤ$
109		uztric	$⊢ (j \in ℤ \land n \in ℤ) \to (n \in ℤ_{\geq j} \lor j \in ℤ_{\geq n})$
110	107 108 109	syl2an	$⊢ (j \in ℕ \land n \in ℕ) \to (n \in ℤ_{\geq j} \lor j \in ℤ_{\geq n})$
111	106 110	sylan	$⊢ ((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in ℕ) \to (n \in ℤ_{\geq j} \lor j \in ℤ_{\geq n})$
112	90 104 111	mpjaodan	$⊢ ((((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \land n \in ℕ) \to F (n) \in (⋃ s \cup w)$
113	112	ralrimiva	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to \forall n \in ℕ F (n) \in (⋃ s \cup w)$
114		fnfvrnss	$⊢ (F Fn ℕ \land \forall n \in ℕ F (n) \in (⋃ s \cup w)) \to ran F \subseteq ⋃ s \cup w$
115	81 113 114	syl2anc	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to ran F \subseteq ⋃ s \cup w$
116		elun2	$⊢ A \in w \to A \in (⋃ s \cup w)$
117	116	ad2antlr	$⊢ ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w)) \to A \in (⋃ s \cup w)$
118	117	ad2antlr	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to A \in (⋃ s \cup w)$
119	118	snssd	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to \{A\} \subseteq ⋃ s \cup w$
120	115 119	unssd	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to ran F \cup \{A\} \subseteq ⋃ s \cup w$
121		uniun	$⊢ ⋃ (s \cup \{w\}) = ⋃ s \cup ⋃ \{w\}$
122		unisnv	$⊢ ⋃ \{w\} = w$
123	122	uneq2i	$⊢ ⋃ s \cup ⋃ \{w\} = ⋃ s \cup w$
124	121 123	eqtri	$⊢ ⋃ (s \cup \{w\}) = ⋃ s \cup w$
125	120 124	sseqtrrdi	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to ran F \cup \{A\} \subseteq ⋃ (s \cup \{w\})$
126		unieq	$⊢ v = s \cup \{w\} \to ⋃ v = ⋃ (s \cup \{w\})$
127	126	sseq2d	$⊢ v = s \cup \{w\} \to (ran F \cup \{A\} \subseteq ⋃ v \leftrightarrow ran F \cup \{A\} \subseteq ⋃ (s \cup \{w\}))$
128	127	rspcev	$⊢ (s \cup \{w\} \in (𝒫 u \cap Fin) \land ran F \cup \{A\} \subseteq ⋃ (s \cup \{w\})) \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v$
129	79 125 128	syl2anc	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \land (s \in (𝒫 u \cap Fin) \land F [(1 \dots j)] \subseteq ⋃ s)) \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v$
130	64 129	rexlimddv	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land ((w \in u \land A \in w) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w))) \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v$
131	130	anassrs	$⊢ (((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \land (j \in ℕ \land \forall k \in ℤ_{\geq j} F (k) \in w)) \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v$
132	23 131	rexlimddv	$⊢ ((φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \land (w \in u \land A \in w)) \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v$
133	14 132	rexlimddv	$⊢ (φ \land (u \in 𝒫 J \land ran F \cup \{A\} \subseteq ⋃ u)) \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v$
134	133	expr	$⊢ (φ \land u \in 𝒫 J) \to (ran F \cup \{A\} \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v)$
135	134	ralrimiva	$⊢ φ \to \forall u \in 𝒫 J (ran F \cup \{A\} \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v)$
136	7	snssd	$⊢ φ \to \{A\} \subseteq X$
137	29 136	unssd	$⊢ φ \to ran F \cup \{A\} \subseteq X$
138	137 55	sseqtrd	$⊢ φ \to ran F \cup \{A\} \subseteq ⋃ J$
139	57	cmpsub	$⊢ (J \in Top \land ran F \cup \{A\} \subseteq ⋃ J) \to (J ↾_{𝑡} (ran F \cup \{A\}) \in Comp \leftrightarrow \forall u \in 𝒫 J (ran F \cup \{A\} \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v))$
140	53 138 139	syl2anc	$⊢ φ \to (J ↾_{𝑡} (ran F \cup \{A\}) \in Comp \leftrightarrow \forall u \in 𝒫 J (ran F \cup \{A\} \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \cup \{A\} \subseteq ⋃ v))$
141	135 140	mpbird	$⊢ φ \to J ↾_{𝑡} (ran F \cup \{A\}) \in Comp$

Metamath Proof Explorer

Theorem 1stckgenlem

Proof