Theorem neibastop2lem 36573

Description: Lemma for neibastop2 36574. (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 4034	. . . . 5 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
3	1, 2	eqsstri 3982	. . . 4 ⊢ 𝑆 ⊆ 𝑋
4		neibastop1.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
5		elpw2g 5280	. . . . 5 ⊢ (𝑋 ∈ 𝑉 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
6	4, 5	syl 17	. . . 4 ⊢ (𝜑 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
7	3, 6	mpbiri 258	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
8		fveq2 6842	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
9	8	ineq1d 4173	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
10	9	neeq1d 2992	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
11	10	rexbidv 3162	. . . . . 6 ⊢ (𝑦 = 𝑥 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
12	11, 1	elrab2 3651	. . . . 5 ⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13		frfnom 8376	. . . . . . . . . 10 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14		neibastop2.g	. . . . . . . . . . 11 ⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
15	14	fneq1i 6597	. . . . . . . . . 10 ⊢ (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
16	13, 15	mpbir 231	. . . . . . . . 9 ⊢ 𝐺 Fn ω
17		fnunirn 7209	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
18	16, 17	ax-mp 5	. . . . . . . 8 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
19		n0 4307	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
20		inss1 4191	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹‘𝑥)
21	20	sseli 3931	. . . . . . . . . . . . . . 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 6873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹‘𝑥) ⊆ ∪ ran 𝐹
28		neibastop1.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
29	28	frnd 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
30	29	difss2d 4093	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
31		sspwuni 5057	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ↔ ∪ ran 𝐹 ⊆ 𝒫 𝑋)
32	30, 31	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
33	32	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
34	27, 33	sstrid 3947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐹‘𝑥) ⊆ 𝒫 𝑋)
35	34	sselda 3935	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ∈ 𝒫 𝑋)
36	35	elpwid 4565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ⊆ 𝑋)
37	36	sselda 3935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ 𝑋)
38	37	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑋)
39		simprlr 780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺‘𝑘))
40		rspe 3228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
41	40	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
42		eliun 4952	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))
43		pweq 4570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
44	43	ineq2d 4174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑓 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
45	44	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
46	45	rexbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑓 → (∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
47	42, 46	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
48	47	rspcev 3578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 ∈ (𝐺‘𝑘) ∧ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
49	39, 41, 48	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
50		eliun 4952	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
51	49, 50	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
52		simpll 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝜑)
53		simprll 779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
54		fvssunirn 6873	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐺‘𝑘) ⊆ ∪ ran 𝐺
55		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = (𝐺‘∅))
56	14	fveq1i 6843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
57		snex 5385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ {𝑈} ∈ V
58		fr0g 8377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
59	57, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
60	56, 59	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐺‘∅) = {𝑈}
61	55, 60	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = {𝑈})
62	61	sseq1d 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = ∅ → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
63		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
64	63	sseq1d 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘𝑘) ⊆ 𝒫 𝑈))
65		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = suc 𝑘 → (𝐺‘𝑛) = (𝐺‘suc 𝑘))
66	65	sseq1d 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = suc 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
67		neibastop2.f	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃))
68		pwidg 4576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ 𝒫 𝑈)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 𝑈 ∈ 𝒫 𝑈)
70	69	snssd 4767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
71		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
72	67	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹‘𝑃))
73	72	pwexd 5326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
74		inss2 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
75		elpwi 4563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑧 ∈ 𝒫 𝑈 → 𝑧 ⊆ 𝑈)
76	75	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝑧 ⊆ 𝑈)
77	76	sspwd 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
78	74, 77	sstrid 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
79	78	ralrimivw 3134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
80		iunss 5002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
81	79, 80	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
82	81	ralrimiva 3130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
83		ssralv 4004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
84	83	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
85	82, 84	mpan9 506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
86		iunss 5002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
87	85, 86	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
88	73, 87	ssexd 5271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V)
89		iuneq1 4965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = 𝑎 → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
90		iuneq1 4965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = (𝐺‘𝑘) → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
91	14, 89, 90	frsucmpt2 8381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ω ∧ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
92	71, 88, 91	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
93	92, 87	eqsstrd 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
94	93	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ ω) → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
95	94	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ω → (𝜑 → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
96	62, 64, 66, 70, 95	finds2 7850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ⊆ 𝒫 𝑈))
97		fvex 6855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐺‘𝑛) ∈ V
98	97	elpw 4560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺‘𝑛) ⊆ 𝒫 𝑈)
99	96, 98	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
100	99	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑛 ∈ ω → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
101	100	ralrimiv 3129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
102		ffnfv 7073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
103	16, 102	mpbiran 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
104	101, 103	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐺:ω⟶𝒫 𝒫 𝑈)
105	104	frnd 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
106		sspwuni 5057	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ↔ ∪ ran 𝐺 ⊆ 𝒫 𝑈)
107	105, 106	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
108	107	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
109	54, 108	sstrid 3947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
110	52, 53, 109, 92	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
111	51, 110	eleqtrrd 2840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
112		peano2 7842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
113	53, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
114		fnfvelrn 7034	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
115	16, 113, 114	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
116		elunii 4870	. . . . . . . . . . . . . . . . . . . . . . 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 4570	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
121	120	ineq2d 4174	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑣 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑣))
122	121	neeq1d 2992	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑣 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅))
123	122	rspcev 3578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
124	118, 119, 123	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
125	1	reqabi 3424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
126	38, 124, 125	sylanbrc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑆)
127	126	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → (((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦 ∈ 𝑆))
128	127	ralimdva 3150	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → (∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆))
129	128	impr 454	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
130		dfss3 3924	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ⊆ 𝑆 ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
131	129, 130	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ⊆ 𝑆)
132		velpw 4561	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝒫 𝑆 ↔ 𝑡 ⊆ 𝑆)
133	131, 132	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
134		inelcm 4419	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝐹‘𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
135	26, 133, 134	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
136	25, 135	rexlimddv 3145	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
137	136	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
138	137	exlimdv 1935	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
139	19, 138	biimtrid 242	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
140	139	rexlimdvaa 3140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
141	18, 140	biimtrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
142	141	rexlimdv 3137	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
143	142	expimpd 453	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144	12, 143	biimtrid 242	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
145	144	ralrimiv 3129	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
146		pweq 4570	. . . . . . 7 ⊢ (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
147	146	ineq2d 4174	. . . . . 6 ⊢ (𝑜 = 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑆))
148	147	neeq1d 2992	. . . . 5 ⊢ (𝑜 = 𝑆 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
149	148	raleqbi1dv 3310	. . . 4 ⊢ (𝑜 = 𝑆 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
150		neibastop1.4	. . . 4 ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}
151	149, 150	elrab2 3651	. . 3 ⊢ (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
152	7, 145, 151	sylanbrc 584	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝐽)
153		neibastop2.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
154		snidg 4619	. . . . . 6 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ {𝑈})
155	67, 154	syl 17	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ {𝑈})
156		peano1 7841	. . . . . . 7 ⊢ ∅ ∈ ω
157		fnfvelrn 7034	. . . . . . 7 ⊢ ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
158	16, 156, 157	mp2an 693	. . . . . 6 ⊢ (𝐺‘∅) ∈ ran 𝐺
159	60, 158	eqeltrri 2834	. . . . 5 ⊢ {𝑈} ∈ ran 𝐺
160		elunii 4870	. . . . 5 ⊢ ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ∈ ∪ ran 𝐺)
161	155, 159, 160	sylancl 587	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ∪ ran 𝐺)
162		inelcm 4419	. . . . 5 ⊢ ((𝑈 ∈ (𝐹‘𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
163	67, 69, 162	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
164		pweq 4570	. . . . . . 7 ⊢ (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
165	164	ineq2d 4174	. . . . . 6 ⊢ (𝑓 = 𝑈 → ((𝐹‘𝑃) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑈))
166	165	neeq1d 2992	. . . . 5 ⊢ (𝑓 = 𝑈 → (((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅))
167	166	rspcev 3578	. . . 4 ⊢ ((𝑈 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
168	161, 163, 167	syl2anc 585	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
169		fveq2 6842	. . . . . . 7 ⊢ (𝑦 = 𝑃 → (𝐹‘𝑦) = (𝐹‘𝑃))
170	169	ineq1d 4173	. . . . . 6 ⊢ (𝑦 = 𝑃 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑓))
171	170	neeq1d 2992	. . . . 5 ⊢ (𝑦 = 𝑃 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
172	171	rexbidv 3162	. . . 4 ⊢ (𝑦 = 𝑃 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
173	172, 1	elrab2 3651	. . 3 ⊢ (𝑃 ∈ 𝑆 ↔ (𝑃 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
174	153, 168, 173	sylanbrc 584	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑆)
175		eluni2 4869	. . . . . . 7 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧)
176		eleq2 2826	. . . . . . . . . 10 ⊢ (𝑧 = (𝐺‘𝑘) → (𝑓 ∈ 𝑧 ↔ 𝑓 ∈ (𝐺‘𝑘)))
177	176	rexrn 7041	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
178	16, 177	ax-mp 5	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
179	104	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
180	179	ffvelcdmda 7038	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ∈ 𝒫 𝒫 𝑈)
181	180	elpwid 4565	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
182	181	sselda 3935	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → 𝑓 ∈ 𝒫 𝑈)
183	182	adantrr 718	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
184	183	elpwid 4565	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑈)
185		neibastop2.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ⊆ 𝑁)
186	185	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈 ⊆ 𝑁)
187	184, 186	sstrd 3946	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑁)
188		n0 4307	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓))
189		elin 3919	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
190		simprrr 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
191	190	elpwid 4565	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ⊆ 𝑓)
192		simpllr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑋)
193		neibastop1.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
194	193	expr 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
195	194	ralrimiva 3130	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
196	195	ad3antrrr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
197		simprrl 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹‘𝑦))
198		fveq2 6842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
199	198	eleq2d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ (𝐹‘𝑥) ↔ 𝑣 ∈ (𝐹‘𝑦)))
200		elequ1 2121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
201	199, 200	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) ↔ (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
202	201	rspcv 3574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) → (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
203	192, 196, 197, 202	syl3c 66	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑣)
204	191, 203	sseldd 3936	. . . . . . . . . . . . . . . 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 3936	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑁)
211	210	exp32 420	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
212	211	rexlimdva 3139	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
213	178, 212	biimtrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
214	175, 213	biimtrid 242	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
215	214	rexlimdv 3137	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))
216	215	3impia 1118	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦 ∈ 𝑁)
217	216	rabssdv 4028	. . 3 ⊢ (𝜑 → {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
218	1, 217	eqsstrid 3974	. 2 ⊢ (𝜑 → 𝑆 ⊆ 𝑁)
219		eleq2 2826	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ 𝑆))
220		sseq1 3961	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑢 ⊆ 𝑁 ↔ 𝑆 ⊆ 𝑁))
221	219, 220	anbi12d 633	. . 3 ⊢ (𝑢 = 𝑆 → ((𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁) ↔ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)))
222	221	rspcev 3578	. 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 2933  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∖ cdif 3900   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  {csn 4582  ∪ cuni 4865  ∪ ciun 4948   ↦ cmpt 5181  ran crn 5633   ↾ cres 5634  suc csuc 6327   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  ωcom 7818  reccrdg 8350

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 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351

This theorem is referenced by:  neibastop2  36574