Theorem neibastop2lem 34476

Description: Lemma for neibastop2 34477. (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 4009	. . . . 5 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
3	1, 2	eqsstri 3951	. . . 4 ⊢ 𝑆 ⊆ 𝑋
4		neibastop1.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
5		elpw2g 5263	. . . . 5 ⊢ (𝑋 ∈ 𝑉 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
6	4, 5	syl 17	. . . 4 ⊢ (𝜑 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
7	3, 6	mpbiri 257	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
8		fveq2 6756	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
9	8	ineq1d 4142	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
10	9	neeq1d 3002	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
11	10	rexbidv 3225	. . . . . 6 ⊢ (𝑦 = 𝑥 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
12	11, 1	elrab2 3620	. . . . 5 ⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13		frfnom 8236	. . . . . . . . . 10 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14		neibastop2.g	. . . . . . . . . . 11 ⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
15	14	fneq1i 6514	. . . . . . . . . 10 ⊢ (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
16	13, 15	mpbir 230	. . . . . . . . 9 ⊢ 𝐺 Fn ω
17		fnunirn 7108	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
18	16, 17	ax-mp 5	. . . . . . . 8 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
19		n0 4277	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
20		inss1 4159	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹‘𝑥)
21	20	sseli 3913	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹‘𝑥))
22		neibastop1.6	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
23	22	anassrs 467	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ (𝐹‘𝑥)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
24	21, 23	sylan2 592	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
25	24	adantrl 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
26		simprl 767	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹‘𝑥))
27		fvssunirn 6785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹‘𝑥) ⊆ ∪ ran 𝐹
28		neibastop1.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
29	28	frnd 6592	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
30	29	difss2d 4065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
31		sspwuni 5025	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ↔ ∪ ran 𝐹 ⊆ 𝒫 𝑋)
32	30, 31	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
33	32	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
34	27, 33	sstrid 3928	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐹‘𝑥) ⊆ 𝒫 𝑋)
35	34	sselda 3917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ∈ 𝒫 𝑋)
36	35	elpwid 4541	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ⊆ 𝑋)
37	36	sselda 3917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ 𝑋)
38	37	adantrr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑋)
39		simprlr 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺‘𝑘))
40		rspe 3232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
41	40	ad2ant2l 742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
42		eliun 4925	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))
43		pweq 4546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
44	43	ineq2d 4143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑓 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
45	44	eleq2d 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
46	45	rexbidv 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑓 → (∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
47	42, 46	syl5bb 282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
48	47	rspcev 3552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 ∈ (𝐺‘𝑘) ∧ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
49	39, 41, 48	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
50		eliun 4925	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
51	49, 50	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
52		simpll 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝜑)
53		simprll 775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
54		fvssunirn 6785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐺‘𝑘) ⊆ ∪ ran 𝐺
55		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = (𝐺‘∅))
56	14	fveq1i 6757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
57		snex 5349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ {𝑈} ∈ V
58		fr0g 8237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
59	57, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
60	56, 59	eqtri 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐺‘∅) = {𝑈}
61	55, 60	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = {𝑈})
62	61	sseq1d 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = ∅ → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
63		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
64	63	sseq1d 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘𝑘) ⊆ 𝒫 𝑈))
65		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = suc 𝑘 → (𝐺‘𝑛) = (𝐺‘suc 𝑘))
66	65	sseq1d 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = suc 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
67		neibastop2.f	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃))
68		pwidg 4552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ 𝒫 𝑈)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 𝑈 ∈ 𝒫 𝑈)
70	69	snssd 4739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
71		simprl 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
72	67	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹‘𝑃))
73	72	pwexd 5297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
74		inss2 4160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
75		elpwi 4539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑧 ∈ 𝒫 𝑈 → 𝑧 ⊆ 𝑈)
76	75	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝑧 ⊆ 𝑈)
77	76	sspwd 4545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
78	74, 77	sstrid 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
79	78	ralrimivw 3108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
80		iunss 4971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
81	79, 80	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
82	81	ralrimiva 3107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
83		ssralv 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
84	83	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
85	82, 84	mpan9 506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
86		iunss 4971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
87	85, 86	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
88	73, 87	ssexd 5243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V)
89		iuneq1 4937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = 𝑎 → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
90		iuneq1 4937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = (𝐺‘𝑘) → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
91	14, 89, 90	frsucmpt2 8241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ω ∧ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
92	71, 88, 91	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
93	92, 87	eqsstrd 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
94	93	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ ω) → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
95	94	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ω → (𝜑 → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
96	62, 64, 66, 70, 95	finds2 7721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ⊆ 𝒫 𝑈))
97		fvex 6769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐺‘𝑛) ∈ V
98	97	elpw 4534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺‘𝑛) ⊆ 𝒫 𝑈)
99	96, 98	syl6ibr 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
100	99	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑛 ∈ ω → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
101	100	ralrimiv 3106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
102		ffnfv 6974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
103	16, 102	mpbiran 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
104	101, 103	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐺:ω⟶𝒫 𝒫 𝑈)
105	104	frnd 6592	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
106		sspwuni 5025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ↔ ∪ ran 𝐺 ⊆ 𝒫 𝑈)
107	105, 106	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
108	107	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
109	54, 108	sstrid 3928	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
110	52, 53, 109, 92	syl12anc 833	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
111	51, 110	eleqtrrd 2842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
112		peano2 7711	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
113	53, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
114		fnfvelrn 6940	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
115	16, 113, 114	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
116		elunii 4841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ∈ ∪ ran 𝐺)
117	111, 115, 116	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ ran 𝐺)
118	117	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ∈ ∪ ran 𝐺)
119		simprr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
120		pweq 4546	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
121	120	ineq2d 4143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑣 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑣))
122	121	neeq1d 3002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑣 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅))
123	122	rspcev 3552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
124	118, 119, 123	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
125	1	rabeq2i 3412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
126	38, 124, 125	sylanbrc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑆)
127	126	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → (((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦 ∈ 𝑆))
128	127	ralimdva 3102	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → (∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆))
129	128	impr 454	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
130		dfss3 3905	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ⊆ 𝑆 ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
131	129, 130	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ⊆ 𝑆)
132		velpw 4535	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝒫 𝑆 ↔ 𝑡 ⊆ 𝑆)
133	131, 132	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
134		inelcm 4395	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝐹‘𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
135	26, 133, 134	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
136	25, 135	rexlimddv 3219	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
137	136	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
138	137	exlimdv 1937	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
139	19, 138	syl5bi 241	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
140	139	rexlimdvaa 3213	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
141	18, 140	syl5bi 241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
142	141	rexlimdv 3211	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
143	142	expimpd 453	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144	12, 143	syl5bi 241	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
145	144	ralrimiv 3106	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
146		pweq 4546	. . . . . . 7 ⊢ (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
147	146	ineq2d 4143	. . . . . 6 ⊢ (𝑜 = 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑆))
148	147	neeq1d 3002	. . . . 5 ⊢ (𝑜 = 𝑆 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
149	148	raleqbi1dv 3331	. . . 4 ⊢ (𝑜 = 𝑆 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
150		neibastop1.4	. . . 4 ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}
151	149, 150	elrab2 3620	. . 3 ⊢ (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
152	7, 145, 151	sylanbrc 582	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝐽)
153		neibastop2.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
154		snidg 4592	. . . . . 6 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ {𝑈})
155	67, 154	syl 17	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ {𝑈})
156		peano1 7710	. . . . . . 7 ⊢ ∅ ∈ ω
157		fnfvelrn 6940	. . . . . . 7 ⊢ ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
158	16, 156, 157	mp2an 688	. . . . . 6 ⊢ (𝐺‘∅) ∈ ran 𝐺
159	60, 158	eqeltrri 2836	. . . . 5 ⊢ {𝑈} ∈ ran 𝐺
160		elunii 4841	. . . . 5 ⊢ ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ∈ ∪ ran 𝐺)
161	155, 159, 160	sylancl 585	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ∪ ran 𝐺)
162		inelcm 4395	. . . . 5 ⊢ ((𝑈 ∈ (𝐹‘𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
163	67, 69, 162	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
164		pweq 4546	. . . . . . 7 ⊢ (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
165	164	ineq2d 4143	. . . . . 6 ⊢ (𝑓 = 𝑈 → ((𝐹‘𝑃) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑈))
166	165	neeq1d 3002	. . . . 5 ⊢ (𝑓 = 𝑈 → (((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅))
167	166	rspcev 3552	. . . 4 ⊢ ((𝑈 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
168	161, 163, 167	syl2anc 583	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
169		fveq2 6756	. . . . . . 7 ⊢ (𝑦 = 𝑃 → (𝐹‘𝑦) = (𝐹‘𝑃))
170	169	ineq1d 4142	. . . . . 6 ⊢ (𝑦 = 𝑃 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑓))
171	170	neeq1d 3002	. . . . 5 ⊢ (𝑦 = 𝑃 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
172	171	rexbidv 3225	. . . 4 ⊢ (𝑦 = 𝑃 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
173	172, 1	elrab2 3620	. . 3 ⊢ (𝑃 ∈ 𝑆 ↔ (𝑃 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
174	153, 168, 173	sylanbrc 582	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑆)
175		eluni2 4840	. . . . . . 7 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧)
176		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑧 = (𝐺‘𝑘) → (𝑓 ∈ 𝑧 ↔ 𝑓 ∈ (𝐺‘𝑘)))
177	176	rexrn 6945	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
178	16, 177	ax-mp 5	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
179	104	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
180	179	ffvelrnda 6943	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ∈ 𝒫 𝒫 𝑈)
181	180	elpwid 4541	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
182	181	sselda 3917	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → 𝑓 ∈ 𝒫 𝑈)
183	182	adantrr 713	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
184	183	elpwid 4541	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑈)
185		neibastop2.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ⊆ 𝑁)
186	185	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈 ⊆ 𝑁)
187	184, 186	sstrd 3927	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑁)
188		n0 4277	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓))
189		elin 3899	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
190		simprrr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
191	190	elpwid 4541	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ⊆ 𝑓)
192		simpllr 772	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑋)
193		neibastop1.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
194	193	expr 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
195	194	ralrimiva 3107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
196	195	ad3antrrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
197		simprrl 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹‘𝑦))
198		fveq2 6756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
199	198	eleq2d 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ (𝐹‘𝑥) ↔ 𝑣 ∈ (𝐹‘𝑦)))
200		elequ1 2115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
201	199, 200	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) ↔ (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
202	201	rspcv 3547	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) → (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
203	192, 196, 197, 202	syl3c 66	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑣)
204	191, 203	sseldd 3918	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑓)
205	204	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → ((𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
206	189, 205	syl5bi 241	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
207	206	exlimdv 1937	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
208	188, 207	syl5bi 241	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑓))
209	208	impr 454	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑓)
210	187, 209	sseldd 3918	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑁)
211	210	exp32 420	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
212	211	rexlimdva 3212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
213	178, 212	syl5bi 241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
214	175, 213	syl5bi 241	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
215	214	rexlimdv 3211	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))
216	215	3impia 1115	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦 ∈ 𝑁)
217	216	rabssdv 4004	. . 3 ⊢ (𝜑 → {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
218	1, 217	eqsstrid 3965	. 2 ⊢ (𝜑 → 𝑆 ⊆ 𝑁)
219		eleq2 2827	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ 𝑆))
220		sseq1 3942	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑢 ⊆ 𝑁 ↔ 𝑆 ⊆ 𝑁))
221	219, 220	anbi12d 630	. . 3 ⊢ (𝑢 = 𝑆 → ((𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁) ↔ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)))
222	221	rspcev 3552	. 2 ⊢ ((𝑆 ∈ 𝐽 ∧ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
223	152, 174, 218, 222	syl12anc 833	1 ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ∖ cdif 3880   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  {csn 4558  ∪ cuni 4836  ∪ ciun 4921   ↦ cmpt 5153  ran crn 5581   ↾ cres 5582  suc csuc 6253   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418  ωcom 7687  reccrdg 8211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212

This theorem is referenced by:  neibastop2  34477