Theorem neibastop2lem 36542

Description: Lemma for neibastop2 36543. (Contributed by Jeff Hankins, 12-Sep-2009.)

Hypotheses

Ref	Expression
neibastop1.1	⊢ (𝜑 → 𝑋 ∈ 𝑉)
neibastop1.2	⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
neibastop1.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
neibastop1.4	⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}
neibastop1.5	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
neibastop1.6	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
neibastop2.p	⊢ (𝜑 → 𝑃 ∈ 𝑋)
neibastop2.n	⊢ (𝜑 → 𝑁 ⊆ 𝑋)
neibastop2.f	⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃))
neibastop2.u	⊢ (𝜑 → 𝑈 ⊆ 𝑁)
neibastop2.g	⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
neibastop2.s	⊢ 𝑆 = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}

Assertion

Ref	Expression
neibastop2lem	⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))

Distinct variable groups:   𝑡,𝑓,𝑣,𝑦,𝑧,𝐺   𝑣,𝑢,𝑥,𝑦,𝑧,𝐽   𝑓,𝑜,𝑢,𝑤,𝑥,𝑃,𝑡,𝑣,𝑦,𝑧   𝑓,𝑁,𝑜,𝑡,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧   𝑆,𝑓,𝑜,𝑡,𝑢,𝑣,𝑥,𝑦   𝑈,𝑓,𝑥,𝑦,𝑧   𝑓,𝑎,𝑜,𝑡,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧,𝐹   𝜑,𝑓,𝑜,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝑋,𝑎,𝑓,𝑜,𝑡,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑢,𝑎)   𝑃(𝑎)   𝑆(𝑧,𝑤,𝑎)   𝑈(𝑤,𝑣,𝑢,𝑡,𝑜,𝑎)   𝐺(𝑥,𝑤,𝑢,𝑜,𝑎)   𝐽(𝑤,𝑡,𝑓,𝑜,𝑎)   𝑁(𝑎)   𝑉(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑡,𝑓,𝑜,𝑎)

Proof of Theorem neibastop2lem

Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neibastop2.s	. . . . 5 ⊢ 𝑆 = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}
2		ssrab2 4020	. . . . 5 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
3	1, 2	eqsstri 3968	. . . 4 ⊢ 𝑆 ⊆ 𝑋
4		neibastop1.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
5		elpw2g 5274	. . . . 5 ⊢ (𝑋 ∈ 𝑉 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
6	4, 5	syl 17	. . . 4 ⊢ (𝜑 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
7	3, 6	mpbiri 258	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
8		fveq2 6840	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
9	8	ineq1d 4159	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
10	9	neeq1d 2991	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
11	10	rexbidv 3161	. . . . . 6 ⊢ (𝑦 = 𝑥 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
12	11, 1	elrab2 3637	. . . . 5 ⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13		frfnom 8374	. . . . . . . . . 10 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14		neibastop2.g	. . . . . . . . . . 11 ⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
15	14	fneq1i 6595	. . . . . . . . . 10 ⊢ (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
16	13, 15	mpbir 231	. . . . . . . . 9 ⊢ 𝐺 Fn ω
17		fnunirn 7208	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
18	16, 17	ax-mp 5	. . . . . . . 8 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
19		n0 4293	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
20		inss1 4177	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹‘𝑥)
21	20	sseli 3917	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹‘𝑥))
22		neibastop1.6	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
23	22	anassrs 467	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ (𝐹‘𝑥)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
24	21, 23	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
25	24	adantrl 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
26		simprl 771	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹‘𝑥))
27		fvssunirn 6871	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹‘𝑥) ⊆ ∪ ran 𝐹
28		neibastop1.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
29	28	frnd 6676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
30	29	difss2d 4079	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
31		sspwuni 5042	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ↔ ∪ ran 𝐹 ⊆ 𝒫 𝑋)
32	30, 31	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
33	32	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
34	27, 33	sstrid 3933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐹‘𝑥) ⊆ 𝒫 𝑋)
35	34	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ∈ 𝒫 𝑋)
36	35	elpwid 4550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ⊆ 𝑋)
37	36	sselda 3921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ 𝑋)
38	37	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑋)
39		simprlr 780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺‘𝑘))
40		rspe 3227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
41	40	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
42		eliun 4937	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))
43		pweq 4555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
44	43	ineq2d 4160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑓 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
45	44	eleq2d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
46	45	rexbidv 3161	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑓 → (∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
47	42, 46	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
48	47	rspcev 3564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 ∈ (𝐺‘𝑘) ∧ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
49	39, 41, 48	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
50		eliun 4937	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
51	49, 50	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
52		simpll 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝜑)
53		simprll 779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
54		fvssunirn 6871	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐺‘𝑘) ⊆ ∪ ran 𝐺
55		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = (𝐺‘∅))
56	14	fveq1i 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
57		snex 5381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ {𝑈} ∈ V
58		fr0g 8375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
59	57, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
60	56, 59	eqtri 2759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐺‘∅) = {𝑈}
61	55, 60	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = {𝑈})
62	61	sseq1d 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = ∅ → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
63		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
64	63	sseq1d 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘𝑘) ⊆ 𝒫 𝑈))
65		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = suc 𝑘 → (𝐺‘𝑛) = (𝐺‘suc 𝑘))
66	65	sseq1d 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = suc 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
67		neibastop2.f	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃))
68		pwidg 4561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ 𝒫 𝑈)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 𝑈 ∈ 𝒫 𝑈)
70	69	snssd 4730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
71		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
72	67	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹‘𝑃))
73	72	pwexd 5321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
74		inss2 4178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
75		elpwi 4548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑧 ∈ 𝒫 𝑈 → 𝑧 ⊆ 𝑈)
76	75	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝑧 ⊆ 𝑈)
77	76	sspwd 4554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
78	74, 77	sstrid 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
79	78	ralrimivw 3133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
80		iunss 4987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
81	79, 80	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
82	81	ralrimiva 3129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
83		ssralv 3990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
84	83	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
85	82, 84	mpan9 506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
86		iunss 4987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
87	85, 86	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
88	73, 87	ssexd 5265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V)
89		iuneq1 4950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = 𝑎 → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
90		iuneq1 4950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = (𝐺‘𝑘) → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
91	14, 89, 90	frsucmpt2 8379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ω ∧ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
92	71, 88, 91	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
93	92, 87	eqsstrd 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
94	93	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ ω) → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
95	94	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ω → (𝜑 → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
96	62, 64, 66, 70, 95	finds2 7849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ⊆ 𝒫 𝑈))
97		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐺‘𝑛) ∈ V
98	97	elpw 4545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺‘𝑛) ⊆ 𝒫 𝑈)
99	96, 98	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
100	99	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑛 ∈ ω → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
101	100	ralrimiv 3128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
102		ffnfv 7071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
103	16, 102	mpbiran 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
104	101, 103	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐺:ω⟶𝒫 𝒫 𝑈)
105	104	frnd 6676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
106		sspwuni 5042	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ↔ ∪ ran 𝐺 ⊆ 𝒫 𝑈)
107	105, 106	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
108	107	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
109	54, 108	sstrid 3933	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
110	52, 53, 109, 92	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
111	51, 110	eleqtrrd 2839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
112		peano2 7841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
113	53, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
114		fnfvelrn 7032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
115	16, 113, 114	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
116		elunii 4855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ∈ ∪ ran 𝐺)
117	111, 115, 116	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ ran 𝐺)
118	117	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ∈ ∪ ran 𝐺)
119		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
120		pweq 4555	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
121	120	ineq2d 4160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑣 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑣))
122	121	neeq1d 2991	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑣 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅))
123	122	rspcev 3564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
124	118, 119, 123	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
125	1	reqabi 3412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
126	38, 124, 125	sylanbrc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑆)
127	126	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → (((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦 ∈ 𝑆))
128	127	ralimdva 3149	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → (∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆))
129	128	impr 454	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
130		dfss3 3910	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ⊆ 𝑆 ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
131	129, 130	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ⊆ 𝑆)
132		velpw 4546	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝒫 𝑆 ↔ 𝑡 ⊆ 𝑆)
133	131, 132	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
134		inelcm 4405	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝐹‘𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
135	26, 133, 134	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
136	25, 135	rexlimddv 3144	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
137	136	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
138	137	exlimdv 1935	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
139	19, 138	biimtrid 242	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
140	139	rexlimdvaa 3139	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
141	18, 140	biimtrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
142	141	rexlimdv 3136	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
143	142	expimpd 453	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144	12, 143	biimtrid 242	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
145	144	ralrimiv 3128	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
146		pweq 4555	. . . . . . 7 ⊢ (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
147	146	ineq2d 4160	. . . . . 6 ⊢ (𝑜 = 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑆))
148	147	neeq1d 2991	. . . . 5 ⊢ (𝑜 = 𝑆 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
149	148	raleqbi1dv 3305	. . . 4 ⊢ (𝑜 = 𝑆 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
150		neibastop1.4	. . . 4 ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}
151	149, 150	elrab2 3637	. . 3 ⊢ (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
152	7, 145, 151	sylanbrc 584	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝐽)
153		neibastop2.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
154		snidg 4604	. . . . . 6 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ {𝑈})
155	67, 154	syl 17	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ {𝑈})
156		peano1 7840	. . . . . . 7 ⊢ ∅ ∈ ω
157		fnfvelrn 7032	. . . . . . 7 ⊢ ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
158	16, 156, 157	mp2an 693	. . . . . 6 ⊢ (𝐺‘∅) ∈ ran 𝐺
159	60, 158	eqeltrri 2833	. . . . 5 ⊢ {𝑈} ∈ ran 𝐺
160		elunii 4855	. . . . 5 ⊢ ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ∈ ∪ ran 𝐺)
161	155, 159, 160	sylancl 587	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ∪ ran 𝐺)
162		inelcm 4405	. . . . 5 ⊢ ((𝑈 ∈ (𝐹‘𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
163	67, 69, 162	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
164		pweq 4555	. . . . . . 7 ⊢ (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
165	164	ineq2d 4160	. . . . . 6 ⊢ (𝑓 = 𝑈 → ((𝐹‘𝑃) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑈))
166	165	neeq1d 2991	. . . . 5 ⊢ (𝑓 = 𝑈 → (((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅))
167	166	rspcev 3564	. . . 4 ⊢ ((𝑈 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
168	161, 163, 167	syl2anc 585	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
169		fveq2 6840	. . . . . . 7 ⊢ (𝑦 = 𝑃 → (𝐹‘𝑦) = (𝐹‘𝑃))
170	169	ineq1d 4159	. . . . . 6 ⊢ (𝑦 = 𝑃 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑓))
171	170	neeq1d 2991	. . . . 5 ⊢ (𝑦 = 𝑃 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
172	171	rexbidv 3161	. . . 4 ⊢ (𝑦 = 𝑃 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
173	172, 1	elrab2 3637	. . 3 ⊢ (𝑃 ∈ 𝑆 ↔ (𝑃 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
174	153, 168, 173	sylanbrc 584	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑆)
175		eluni2 4854	. . . . . . 7 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧)
176		eleq2 2825	. . . . . . . . . 10 ⊢ (𝑧 = (𝐺‘𝑘) → (𝑓 ∈ 𝑧 ↔ 𝑓 ∈ (𝐺‘𝑘)))
177	176	rexrn 7039	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
178	16, 177	ax-mp 5	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
179	104	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
180	179	ffvelcdmda 7036	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ∈ 𝒫 𝒫 𝑈)
181	180	elpwid 4550	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
182	181	sselda 3921	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → 𝑓 ∈ 𝒫 𝑈)
183	182	adantrr 718	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
184	183	elpwid 4550	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑈)
185		neibastop2.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ⊆ 𝑁)
186	185	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈 ⊆ 𝑁)
187	184, 186	sstrd 3932	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑁)
188		n0 4293	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓))
189		elin 3905	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
190		simprrr 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
191	190	elpwid 4550	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ⊆ 𝑓)
192		simpllr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑋)
193		neibastop1.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
194	193	expr 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
195	194	ralrimiva 3129	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
196	195	ad3antrrr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
197		simprrl 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹‘𝑦))
198		fveq2 6840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
199	198	eleq2d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ (𝐹‘𝑥) ↔ 𝑣 ∈ (𝐹‘𝑦)))
200		elequ1 2121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
201	199, 200	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) ↔ (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
202	201	rspcv 3560	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) → (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
203	192, 196, 197, 202	syl3c 66	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑣)
204	191, 203	sseldd 3922	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑓)
205	204	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → ((𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
206	189, 205	biimtrid 242	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
207	206	exlimdv 1935	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
208	188, 207	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑓))
209	208	impr 454	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑓)
210	187, 209	sseldd 3922	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑁)
211	210	exp32 420	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
212	211	rexlimdva 3138	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
213	178, 212	biimtrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
214	175, 213	biimtrid 242	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
215	214	rexlimdv 3136	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))
216	215	3impia 1118	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦 ∈ 𝑁)
217	216	rabssdv 4014	. . 3 ⊢ (𝜑 → {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
218	1, 217	eqsstrid 3960	. 2 ⊢ (𝜑 → 𝑆 ⊆ 𝑁)
219		eleq2 2825	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ 𝑆))
220		sseq1 3947	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑢 ⊆ 𝑁 ↔ 𝑆 ⊆ 𝑁))
221	219, 220	anbi12d 633	. . 3 ⊢ (𝑢 = 𝑆 → ((𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁) ↔ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)))
222	221	rspcev 3564	. 2 ⊢ ((𝑆 ∈ 𝐽 ∧ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
223	152, 174, 218, 222	syl12anc 837	1 ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  {crab 3389  Vcvv 3429   ∖ cdif 3886   ∩ cin 3888   ⊆ wss 3889  ∅c0 4273  𝒫 cpw 4541  {csn 4567  ∪ cuni 4850  ∪ ciun 4933   ↦ cmpt 5166  ran crn 5632   ↾ cres 5633  suc csuc 6325   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498  ωcom 7817  reccrdg 8348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349

This theorem is referenced by:  neibastop2  36543