neibastop2lem

	Ref	Expression
Hypotheses	neibastop1.1	$⊢ φ \to X \in V$
	neibastop1.2	$⊢ φ \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
	neibastop1.3	$⊢ (φ \land (x \in X \land v \in F (x) \land w \in F (x))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
	neibastop1.4	$⊢ J = \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\}$
	neibastop1.5	$⊢ (φ \land (x \in X \land v \in F (x))) \to x \in v$
	neibastop1.6	$⊢ (φ \land (x \in X \land v \in F (x))) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
	neibastop2.p	$⊢ φ \to P \in X$
	neibastop2.n	$⊢ φ \to N \subseteq X$
	neibastop2.f	$⊢ φ \to U \in F (P)$
	neibastop2.u	$⊢ φ \to U \subseteq N$
	neibastop2.g	$⊢ G = {rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{U\}) ↾}_{ω}$
	neibastop2.s	$⊢ S = \{y \in X \| \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset\}$
Assertion	neibastop2lem	$⊢ φ \to \exists u \in J (P \in u \land u \subseteq N)$

Proof

Step	Hyp	Ref	Expression
1		neibastop1.1	$⊢ φ \to X \in V$
2		neibastop1.2	$⊢ φ \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
3		neibastop1.3	$⊢ (φ \land (x \in X \land v \in F (x) \land w \in F (x))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
4		neibastop1.4	$⊢ J = \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\}$
5		neibastop1.5	$⊢ (φ \land (x \in X \land v \in F (x))) \to x \in v$
6		neibastop1.6	$⊢ (φ \land (x \in X \land v \in F (x))) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
7		neibastop2.p	$⊢ φ \to P \in X$
8		neibastop2.n	$⊢ φ \to N \subseteq X$
9		neibastop2.f	$⊢ φ \to U \in F (P)$
10		neibastop2.u	$⊢ φ \to U \subseteq N$
11		neibastop2.g	$⊢ G = {rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{U\}) ↾}_{ω}$
12		neibastop2.s	$⊢ S = \{y \in X \| \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset\}$
13		ssrab2	$⊢ \{y \in X \| \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset\} \subseteq X$
14	12 13	eqsstri	$⊢ S \subseteq X$
15		elpw2g	$⊢ X \in V \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
16	1 15	syl	$⊢ φ \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
17	14 16	mpbiri	$⊢ φ \to S \in 𝒫 X$
18		fveq2	$⊢ y = x \to F (y) = F (x)$
19	18	ineq1d	$⊢ y = x \to F (y) \cap 𝒫 f = F (x) \cap 𝒫 f$
20	19	neeq1d	$⊢ y = x \to (F (y) \cap 𝒫 f \neq \emptyset \leftrightarrow F (x) \cap 𝒫 f \neq \emptyset)$
21	20	rexbidv	$⊢ y = x \to (\exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset \leftrightarrow \exists f \in ⋃ ran G F (x) \cap 𝒫 f \neq \emptyset)$
22	21 12	elrab2	$⊢ x \in S \leftrightarrow (x \in X \land \exists f \in ⋃ ran G F (x) \cap 𝒫 f \neq \emptyset)$
23		frfnom	$⊢ ({rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{U\}) ↾}_{ω}) Fn ω$
24	11	fneq1i	$⊢ G Fn ω \leftrightarrow ({rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{U\}) ↾}_{ω}) Fn ω$
25	23 24	mpbir	$⊢ G Fn ω$
26		fnunirn	$⊢ G Fn ω \to (f \in ⋃ ran G \leftrightarrow \exists k \in ω f \in G (k))$
27	25 26	ax-mp	$⊢ f \in ⋃ ran G \leftrightarrow \exists k \in ω f \in G (k)$
28		n0	$⊢ F (x) \cap 𝒫 f \neq \emptyset \leftrightarrow \exists v v \in (F (x) \cap 𝒫 f)$
29		inss1	$⊢ F (x) \cap 𝒫 f \subseteq F (x)$
30	29	sseli	$⊢ v \in (F (x) \cap 𝒫 f) \to v \in F (x)$
31	6	anassrs	$⊢ ((φ \land x \in X) \land v \in F (x)) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
32	30 31	sylan2	$⊢ ((φ \land x \in X) \land v \in (F (x) \cap 𝒫 f)) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
33	32	adantrl	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
34		simprl	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land (t \in F (x) \land \forall y \in t F (y) \cap 𝒫 v \neq \emptyset)) \to t \in F (x)$
35		fvssunirn	$⊢ F (x) \subseteq ⋃ ran F$
36	2	frnd	$⊢ φ \to ran F \subseteq 𝒫 𝒫 X ∖ \{\emptyset\}$
37	36	difss2d	$⊢ φ \to ran F \subseteq 𝒫 𝒫 X$
38		sspwuni	$⊢ ran F \subseteq 𝒫 𝒫 X \leftrightarrow ⋃ ran F \subseteq 𝒫 X$
39	37 38	sylib	$⊢ φ \to ⋃ ran F \subseteq 𝒫 X$
40	39	ad2antrr	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to ⋃ ran F \subseteq 𝒫 X$
41	35 40	sstrid	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to F (x) \subseteq 𝒫 X$
42	41	sselda	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \to t \in 𝒫 X$
43	42	elpwid	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \to t \subseteq X$
44	43	sselda	$⊢ ((((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \land y \in t) \to y \in X$
45	44	adantrr	$⊢ ((((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \land (y \in t \land F (y) \cap 𝒫 v \neq \emptyset)) \to y \in X$
46		simprlr	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to f \in G (k)$
47		rspe	$⊢ (x \in X \land v \in (F (x) \cap 𝒫 f)) \to \exists x \in X v \in (F (x) \cap 𝒫 f)$
48	47	ad2ant2l	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to \exists x \in X v \in (F (x) \cap 𝒫 f)$
49		eliun	$⊢ v \in ⋃_{x \in X} (F (x) \cap 𝒫 z) \leftrightarrow \exists x \in X v \in (F (x) \cap 𝒫 z)$
50		pweq	$⊢ z = f \to 𝒫 z = 𝒫 f$
51	50	ineq2d	$⊢ z = f \to F (x) \cap 𝒫 z = F (x) \cap 𝒫 f$
52	51	eleq2d	$⊢ z = f \to (v \in (F (x) \cap 𝒫 z) \leftrightarrow v \in (F (x) \cap 𝒫 f))$
53	52	rexbidv	$⊢ z = f \to (\exists x \in X v \in (F (x) \cap 𝒫 z) \leftrightarrow \exists x \in X v \in (F (x) \cap 𝒫 f))$
54	49 53	syl5bb	$⊢ z = f \to (v \in ⋃_{x \in X} (F (x) \cap 𝒫 z) \leftrightarrow \exists x \in X v \in (F (x) \cap 𝒫 f))$
55	54	rspcev	$⊢ (f \in G (k) \land \exists x \in X v \in (F (x) \cap 𝒫 f)) \to \exists z \in G (k) v \in ⋃_{x \in X} (F (x) \cap 𝒫 z)$
56	46 48 55	syl2anc	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to \exists z \in G (k) v \in ⋃_{x \in X} (F (x) \cap 𝒫 z)$
57		eliun	$⊢ v \in ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z) \leftrightarrow \exists z \in G (k) v \in ⋃_{x \in X} (F (x) \cap 𝒫 z)$
58	56 57	sylibr	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to v \in ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
59		simpll	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to φ$
60		simprll	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to k \in ω$
61		fvssunirn	$⊢ G (k) \subseteq ⋃ ran G$
62		fveq2	$⊢ n = \emptyset \to G (n) = G (\emptyset)$
63	11	fveq1i	$⊢ G (\emptyset) = ({rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{U\}) ↾}_{ω}) (\emptyset)$
64		snex	$⊢ \{U\} \in V$
65		fr0g	$⊢ \{U\} \in V \to ({rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{U\}) ↾}_{ω}) (\emptyset) = \{U\}$
66	64 65	ax-mp	$⊢ ({rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{U\}) ↾}_{ω}) (\emptyset) = \{U\}$
67	63 66	eqtri	$⊢ G (\emptyset) = \{U\}$
68	62 67	eqtrdi	$⊢ n = \emptyset \to G (n) = \{U\}$
69	68	sseq1d	$⊢ n = \emptyset \to (G (n) \subseteq 𝒫 U \leftrightarrow \{U\} \subseteq 𝒫 U)$
70		fveq2	$⊢ n = k \to G (n) = G (k)$
71	70	sseq1d	$⊢ n = k \to (G (n) \subseteq 𝒫 U \leftrightarrow G (k) \subseteq 𝒫 U)$
72		fveq2	$⊢ n = suc k \to G (n) = G (suc k)$
73	72	sseq1d	$⊢ n = suc k \to (G (n) \subseteq 𝒫 U \leftrightarrow G (suc k) \subseteq 𝒫 U)$
74		pwidg	$⊢ U \in F (P) \to U \in 𝒫 U$
75	9 74	syl	$⊢ φ \to U \in 𝒫 U$
76	75	snssd	$⊢ φ \to \{U\} \subseteq 𝒫 U$
77		simprl	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to k \in ω$
78	9	adantr	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to U \in F (P)$
79	78	pwexd	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to 𝒫 U \in V$
80		inss2	$⊢ F (x) \cap 𝒫 z \subseteq 𝒫 z$
81		elpwi	$⊢ z \in 𝒫 U \to z \subseteq U$
82	81	adantl	$⊢ (φ \land z \in 𝒫 U) \to z \subseteq U$
83	82	sspwd	$⊢ (φ \land z \in 𝒫 U) \to 𝒫 z \subseteq 𝒫 U$
84	80 83	sstrid	$⊢ (φ \land z \in 𝒫 U) \to F (x) \cap 𝒫 z \subseteq 𝒫 U$
85	84	ralrimivw	$⊢ (φ \land z \in 𝒫 U) \to \forall x \in X F (x) \cap 𝒫 z \subseteq 𝒫 U$
86		iunss	$⊢ ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U \leftrightarrow \forall x \in X F (x) \cap 𝒫 z \subseteq 𝒫 U$
87	85 86	sylibr	$⊢ (φ \land z \in 𝒫 U) \to ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U$
88	87	ralrimiva	$⊢ φ \to \forall z \in 𝒫 U ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U$
89		ssralv	$⊢ G (k) \subseteq 𝒫 U \to (\forall z \in 𝒫 U ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U \to \forall z \in G (k) ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U)$
90	89	adantl	$⊢ (k \in ω \land G (k) \subseteq 𝒫 U) \to (\forall z \in 𝒫 U ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U \to \forall z \in G (k) ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U)$
91	88 90	mpan9	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to \forall z \in G (k) ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U$
92		iunss	$⊢ ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U \leftrightarrow \forall z \in G (k) ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U$
93	91 92	sylibr	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z) \subseteq 𝒫 U$
94	79 93	ssexd	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z) \in V$
95		iuneq1	$⊢ y = a \to ⋃_{z \in y} ⋃_{x \in X} (F (x) \cap 𝒫 z) = ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
96		iuneq1	$⊢ y = G (k) \to ⋃_{z \in y} ⋃_{x \in X} (F (x) \cap 𝒫 z) = ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
97	11 95 96	frsucmpt2	$⊢ (k \in ω \land ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z) \in V) \to G (suc k) = ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
98	77 94 97	syl2anc	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to G (suc k) = ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
99	98 93	eqsstrd	$⊢ (φ \land (k \in ω \land G (k) \subseteq 𝒫 U)) \to G (suc k) \subseteq 𝒫 U$
100	99	expr	$⊢ (φ \land k \in ω) \to (G (k) \subseteq 𝒫 U \to G (suc k) \subseteq 𝒫 U)$
101	100	expcom	$⊢ k \in ω \to (φ \to (G (k) \subseteq 𝒫 U \to G (suc k) \subseteq 𝒫 U))$
102	69 71 73 76 101	finds2	$⊢ n \in ω \to (φ \to G (n) \subseteq 𝒫 U)$
103		fvex	$⊢ G (n) \in V$
104	103	elpw	$⊢ G (n) \in 𝒫 𝒫 U \leftrightarrow G (n) \subseteq 𝒫 U$
105	102 104	syl6ibr	$⊢ n \in ω \to (φ \to G (n) \in 𝒫 𝒫 U)$
106	105	com12	$⊢ φ \to (n \in ω \to G (n) \in 𝒫 𝒫 U)$
107	106	ralrimiv	$⊢ φ \to \forall n \in ω G (n) \in 𝒫 𝒫 U$
108		ffnfv	$⊢ G : ω ⟶ 𝒫 𝒫 U \leftrightarrow (G Fn ω \land \forall n \in ω G (n) \in 𝒫 𝒫 U)$
109	25 108	mpbiran	$⊢ G : ω ⟶ 𝒫 𝒫 U \leftrightarrow \forall n \in ω G (n) \in 𝒫 𝒫 U$
110	107 109	sylibr	$⊢ φ \to G : ω ⟶ 𝒫 𝒫 U$
111	110	frnd	$⊢ φ \to ran G \subseteq 𝒫 𝒫 U$
112		sspwuni	$⊢ ran G \subseteq 𝒫 𝒫 U \leftrightarrow ⋃ ran G \subseteq 𝒫 U$
113	111 112	sylib	$⊢ φ \to ⋃ ran G \subseteq 𝒫 U$
114	113	ad2antrr	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to ⋃ ran G \subseteq 𝒫 U$
115	61 114	sstrid	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to G (k) \subseteq 𝒫 U$
116	59 60 115 98	syl12anc	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to G (suc k) = ⋃_{z \in G (k)} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
117	58 116	eleqtrrd	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to v \in G (suc k)$
118		peano2	$⊢ k \in ω \to suc k \in ω$
119	60 118	syl	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to suc k \in ω$
120		fnfvelrn	$⊢ (G Fn ω \land suc k \in ω) \to G (suc k) \in ran G$
121	25 119 120	sylancr	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to G (suc k) \in ran G$
122		elunii	$⊢ (v \in G (suc k) \land G (suc k) \in ran G) \to v \in ⋃ ran G$
123	117 121 122	syl2anc	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to v \in ⋃ ran G$
124	123	ad2antrr	$⊢ ((((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \land (y \in t \land F (y) \cap 𝒫 v \neq \emptyset)) \to v \in ⋃ ran G$
125		simprr	$⊢ ((((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \land (y \in t \land F (y) \cap 𝒫 v \neq \emptyset)) \to F (y) \cap 𝒫 v \neq \emptyset$
126		pweq	$⊢ f = v \to 𝒫 f = 𝒫 v$
127	126	ineq2d	$⊢ f = v \to F (y) \cap 𝒫 f = F (y) \cap 𝒫 v$
128	127	neeq1d	$⊢ f = v \to (F (y) \cap 𝒫 f \neq \emptyset \leftrightarrow F (y) \cap 𝒫 v \neq \emptyset)$
129	128	rspcev	$⊢ (v \in ⋃ ran G \land F (y) \cap 𝒫 v \neq \emptyset) \to \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset$
130	124 125 129	syl2anc	$⊢ ((((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \land (y \in t \land F (y) \cap 𝒫 v \neq \emptyset)) \to \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset$
131	12	rabeq2i	$⊢ y \in S \leftrightarrow (y \in X \land \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset)$
132	45 130 131	sylanbrc	$⊢ ((((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \land (y \in t \land F (y) \cap 𝒫 v \neq \emptyset)) \to y \in S$
133	132	expr	$⊢ ((((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \land y \in t) \to (F (y) \cap 𝒫 v \neq \emptyset \to y \in S)$
134	133	ralimdva	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land t \in F (x)) \to (\forall y \in t F (y) \cap 𝒫 v \neq \emptyset \to \forall y \in t y \in S)$
135	134	impr	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land (t \in F (x) \land \forall y \in t F (y) \cap 𝒫 v \neq \emptyset)) \to \forall y \in t y \in S$
136		dfss3	$⊢ t \subseteq S \leftrightarrow \forall y \in t y \in S$
137	135 136	sylibr	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land (t \in F (x) \land \forall y \in t F (y) \cap 𝒫 v \neq \emptyset)) \to t \subseteq S$
138		velpw	$⊢ t \in 𝒫 S \leftrightarrow t \subseteq S$
139	137 138	sylibr	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land (t \in F (x) \land \forall y \in t F (y) \cap 𝒫 v \neq \emptyset)) \to t \in 𝒫 S$
140		inelcm	$⊢ (t \in F (x) \land t \in 𝒫 S) \to F (x) \cap 𝒫 S \neq \emptyset$
141	34 139 140	syl2anc	$⊢ (((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \land (t \in F (x) \land \forall y \in t F (y) \cap 𝒫 v \neq \emptyset)) \to F (x) \cap 𝒫 S \neq \emptyset$
142	33 141	rexlimddv	$⊢ ((φ \land x \in X) \land ((k \in ω \land f \in G (k)) \land v \in (F (x) \cap 𝒫 f))) \to F (x) \cap 𝒫 S \neq \emptyset$
143	142	expr	$⊢ ((φ \land x \in X) \land (k \in ω \land f \in G (k))) \to (v \in (F (x) \cap 𝒫 f) \to F (x) \cap 𝒫 S \neq \emptyset)$
144	143	exlimdv	$⊢ ((φ \land x \in X) \land (k \in ω \land f \in G (k))) \to (\exists v v \in (F (x) \cap 𝒫 f) \to F (x) \cap 𝒫 S \neq \emptyset)$
145	28 144	syl5bi	$⊢ ((φ \land x \in X) \land (k \in ω \land f \in G (k))) \to (F (x) \cap 𝒫 f \neq \emptyset \to F (x) \cap 𝒫 S \neq \emptyset)$
146	145	rexlimdvaa	$⊢ (φ \land x \in X) \to (\exists k \in ω f \in G (k) \to (F (x) \cap 𝒫 f \neq \emptyset \to F (x) \cap 𝒫 S \neq \emptyset))$
147	27 146	syl5bi	$⊢ (φ \land x \in X) \to (f \in ⋃ ran G \to (F (x) \cap 𝒫 f \neq \emptyset \to F (x) \cap 𝒫 S \neq \emptyset))$
148	147	rexlimdv	$⊢ (φ \land x \in X) \to (\exists f \in ⋃ ran G F (x) \cap 𝒫 f \neq \emptyset \to F (x) \cap 𝒫 S \neq \emptyset)$
149	148	expimpd	$⊢ φ \to ((x \in X \land \exists f \in ⋃ ran G F (x) \cap 𝒫 f \neq \emptyset) \to F (x) \cap 𝒫 S \neq \emptyset)$
150	22 149	syl5bi	$⊢ φ \to (x \in S \to F (x) \cap 𝒫 S \neq \emptyset)$
151	150	ralrimiv	$⊢ φ \to \forall x \in S F (x) \cap 𝒫 S \neq \emptyset$
152		pweq	$⊢ o = S \to 𝒫 o = 𝒫 S$
153	152	ineq2d	$⊢ o = S \to F (x) \cap 𝒫 o = F (x) \cap 𝒫 S$
154	153	neeq1d	$⊢ o = S \to (F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow F (x) \cap 𝒫 S \neq \emptyset)$
155	154	raleqbi1dv	$⊢ o = S \to (\forall x \in o F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow \forall x \in S F (x) \cap 𝒫 S \neq \emptyset)$
156	155 4	elrab2	$⊢ S \in J \leftrightarrow (S \in 𝒫 X \land \forall x \in S F (x) \cap 𝒫 S \neq \emptyset)$
157	17 151 156	sylanbrc	$⊢ φ \to S \in J$
158		snidg	$⊢ U \in F (P) \to U \in \{U\}$
159	9 158	syl	$⊢ φ \to U \in \{U\}$
160		peano1	$⊢ \emptyset \in ω$
161		fnfvelrn	$⊢ (G Fn ω \land \emptyset \in ω) \to G (\emptyset) \in ran G$
162	25 160 161	mp2an	$⊢ G (\emptyset) \in ran G$
163	67 162	eqeltrri	$⊢ \{U\} \in ran G$
164		elunii	$⊢ (U \in \{U\} \land \{U\} \in ran G) \to U \in ⋃ ran G$
165	159 163 164	sylancl	$⊢ φ \to U \in ⋃ ran G$
166		inelcm	$⊢ (U \in F (P) \land U \in 𝒫 U) \to F (P) \cap 𝒫 U \neq \emptyset$
167	9 75 166	syl2anc	$⊢ φ \to F (P) \cap 𝒫 U \neq \emptyset$
168		pweq	$⊢ f = U \to 𝒫 f = 𝒫 U$
169	168	ineq2d	$⊢ f = U \to F (P) \cap 𝒫 f = F (P) \cap 𝒫 U$
170	169	neeq1d	$⊢ f = U \to (F (P) \cap 𝒫 f \neq \emptyset \leftrightarrow F (P) \cap 𝒫 U \neq \emptyset)$
171	170	rspcev	$⊢ (U \in ⋃ ran G \land F (P) \cap 𝒫 U \neq \emptyset) \to \exists f \in ⋃ ran G F (P) \cap 𝒫 f \neq \emptyset$
172	165 167 171	syl2anc	$⊢ φ \to \exists f \in ⋃ ran G F (P) \cap 𝒫 f \neq \emptyset$
173		fveq2	$⊢ y = P \to F (y) = F (P)$
174	173	ineq1d	$⊢ y = P \to F (y) \cap 𝒫 f = F (P) \cap 𝒫 f$
175	174	neeq1d	$⊢ y = P \to (F (y) \cap 𝒫 f \neq \emptyset \leftrightarrow F (P) \cap 𝒫 f \neq \emptyset)$
176	175	rexbidv	$⊢ y = P \to (\exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset \leftrightarrow \exists f \in ⋃ ran G F (P) \cap 𝒫 f \neq \emptyset)$
177	176 12	elrab2	$⊢ P \in S \leftrightarrow (P \in X \land \exists f \in ⋃ ran G F (P) \cap 𝒫 f \neq \emptyset)$
178	7 172 177	sylanbrc	$⊢ φ \to P \in S$
179		eluni2	$⊢ f \in ⋃ ran G \leftrightarrow \exists z \in ran G f \in z$
180		eleq2	$⊢ z = G (k) \to (f \in z \leftrightarrow f \in G (k))$
181	180	rexrn	$⊢ G Fn ω \to (\exists z \in ran G f \in z \leftrightarrow \exists k \in ω f \in G (k))$
182	25 181	ax-mp	$⊢ \exists z \in ran G f \in z \leftrightarrow \exists k \in ω f \in G (k)$
183	110	adantr	$⊢ (φ \land y \in X) \to G : ω ⟶ 𝒫 𝒫 U$
184	183	ffvelrnda	$⊢ ((φ \land y \in X) \land k \in ω) \to G (k) \in 𝒫 𝒫 U$
185	184	elpwid	$⊢ ((φ \land y \in X) \land k \in ω) \to G (k) \subseteq 𝒫 U$
186	185	sselda	$⊢ (((φ \land y \in X) \land k \in ω) \land f \in G (k)) \to f \in 𝒫 U$
187	186	adantrr	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land F (y) \cap 𝒫 f \neq \emptyset)) \to f \in 𝒫 U$
188	187	elpwid	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land F (y) \cap 𝒫 f \neq \emptyset)) \to f \subseteq U$
189	10	ad3antrrr	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land F (y) \cap 𝒫 f \neq \emptyset)) \to U \subseteq N$
190	188 189	sstrd	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land F (y) \cap 𝒫 f \neq \emptyset)) \to f \subseteq N$
191		n0	$⊢ F (y) \cap 𝒫 f \neq \emptyset \leftrightarrow \exists v v \in (F (y) \cap 𝒫 f)$
192		elin	$⊢ v \in (F (y) \cap 𝒫 f) \leftrightarrow (v \in F (y) \land v \in 𝒫 f)$
193		simprrr	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land (v \in F (y) \land v \in 𝒫 f))) \to v \in 𝒫 f$
194	193	elpwid	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land (v \in F (y) \land v \in 𝒫 f))) \to v \subseteq f$
195		simpllr	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land (v \in F (y) \land v \in 𝒫 f))) \to y \in X$
196	5	expr	$⊢ (φ \land x \in X) \to (v \in F (x) \to x \in v)$
197	196	ralrimiva	$⊢ φ \to \forall x \in X (v \in F (x) \to x \in v)$
198	197	ad3antrrr	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land (v \in F (y) \land v \in 𝒫 f))) \to \forall x \in X (v \in F (x) \to x \in v)$
199		simprrl	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land (v \in F (y) \land v \in 𝒫 f))) \to v \in F (y)$
200		fveq2	$⊢ x = y \to F (x) = F (y)$
201	200	eleq2d	$⊢ x = y \to (v \in F (x) \leftrightarrow v \in F (y))$
202		elequ1	$⊢ x = y \to (x \in v \leftrightarrow y \in v)$
203	201 202	imbi12d	$⊢ x = y \to ((v \in F (x) \to x \in v) \leftrightarrow (v \in F (y) \to y \in v))$
204	203	rspcv	$⊢ y \in X \to (\forall x \in X (v \in F (x) \to x \in v) \to (v \in F (y) \to y \in v))$
205	195 198 199 204	syl3c	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land (v \in F (y) \land v \in 𝒫 f))) \to y \in v$
206	194 205	sseldd	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land (v \in F (y) \land v \in 𝒫 f))) \to y \in f$
207	206	expr	$⊢ (((φ \land y \in X) \land k \in ω) \land f \in G (k)) \to ((v \in F (y) \land v \in 𝒫 f) \to y \in f)$
208	192 207	syl5bi	$⊢ (((φ \land y \in X) \land k \in ω) \land f \in G (k)) \to (v \in (F (y) \cap 𝒫 f) \to y \in f)$
209	208	exlimdv	$⊢ (((φ \land y \in X) \land k \in ω) \land f \in G (k)) \to (\exists v v \in (F (y) \cap 𝒫 f) \to y \in f)$
210	191 209	syl5bi	$⊢ (((φ \land y \in X) \land k \in ω) \land f \in G (k)) \to (F (y) \cap 𝒫 f \neq \emptyset \to y \in f)$
211	210	impr	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land F (y) \cap 𝒫 f \neq \emptyset)) \to y \in f$
212	190 211	sseldd	$⊢ (((φ \land y \in X) \land k \in ω) \land (f \in G (k) \land F (y) \cap 𝒫 f \neq \emptyset)) \to y \in N$
213	212	exp32	$⊢ ((φ \land y \in X) \land k \in ω) \to (f \in G (k) \to (F (y) \cap 𝒫 f \neq \emptyset \to y \in N))$
214	213	rexlimdva	$⊢ (φ \land y \in X) \to (\exists k \in ω f \in G (k) \to (F (y) \cap 𝒫 f \neq \emptyset \to y \in N))$
215	182 214	syl5bi	$⊢ (φ \land y \in X) \to (\exists z \in ran G f \in z \to (F (y) \cap 𝒫 f \neq \emptyset \to y \in N))$
216	179 215	syl5bi	$⊢ (φ \land y \in X) \to (f \in ⋃ ran G \to (F (y) \cap 𝒫 f \neq \emptyset \to y \in N))$
217	216	rexlimdv	$⊢ (φ \land y \in X) \to (\exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset \to y \in N)$
218	217	3impia	$⊢ (φ \land y \in X \land \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset) \to y \in N$
219	218	rabssdv	$⊢ φ \to \{y \in X \| \exists f \in ⋃ ran G F (y) \cap 𝒫 f \neq \emptyset\} \subseteq N$
220	12 219	eqsstrid	$⊢ φ \to S \subseteq N$
221		eleq2	$⊢ u = S \to (P \in u \leftrightarrow P \in S)$
222		sseq1	$⊢ u = S \to (u \subseteq N \leftrightarrow S \subseteq N)$
223	221 222	anbi12d	$⊢ u = S \to ((P \in u \land u \subseteq N) \leftrightarrow (P \in S \land S \subseteq N))$
224	223	rspcev	$⊢ (S \in J \land (P \in S \land S \subseteq N)) \to \exists u \in J (P \in u \land u \subseteq N)$
225	157 178 220 224	syl12anc	$⊢ φ \to \exists u \in J (P \in u \land u \subseteq N)$

Metamath Proof Explorer

Theorem neibastop2lem

Proof