Theorem neibastop2lem 36680

Description: Lemma for neibastop2 36681. (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 4031	. . . . 5 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
3	1, 2	eqsstri 3980	. . . 4 ⊢ 𝑆 ⊆ 𝑋
4		neibastop1.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
5		elpw2g 5286	. . . . 5 ⊢ (𝑋 ∈ 𝑉 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
6	4, 5	syl 17	. . . 4 ⊢ (𝜑 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
7	3, 6	mpbiri 260	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
8		fveq2 6861	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
9	8	ineq1d 4169	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
10	9	neeq1d 3015	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
11	10	rexbidv 3185	. . . . . 6 ⊢ (𝑦 = 𝑥 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
12	11, 1	elrab2 3652	. . . . 5 ⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13		frfnom 8399	. . . . . . . . . 10 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14		neibastop2.g	. . . . . . . . . . 11 ⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
15	14	fneq1i 6612	. . . . . . . . . 10 ⊢ (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
16	13, 15	mpbir 233	. . . . . . . . 9 ⊢ 𝐺 Fn ω
17		fnunirn 7231	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
18	16, 17	ax-mp 5	. . . . . . . 8 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
19		n0 4303	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
20		inss1 4186	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹‘𝑥)
21	20	sseli 3930	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹‘𝑥))
22		neibastop1.6	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
23	22	anassrs 471	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ (𝐹‘𝑥)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
24	21, 23	sylan2 602	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
25	24	adantrl 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
26		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹‘𝑥))
27		fvssunirn 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹‘𝑥) ⊆ ∪ ran 𝐹
28		neibastop1.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
29	28	frnd 6694	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
30	29	difss2d 4090	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
31		sspwuni 5054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ↔ ∪ ran 𝐹 ⊆ 𝒫 𝑋)
32	30, 31	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
33	32	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐹 ⊆ 𝒫 𝑋)
34	27, 33	sstrid 3945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐹‘𝑥) ⊆ 𝒫 𝑋)
35	34	sselda 3934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ∈ 𝒫 𝑋)
36	35	elpwid 4561	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ⊆ 𝑋)
37	36	sselda 3934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ 𝑋)
38	37	adantrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑋)
39		simprlr 789	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺‘𝑘))
40		rspe 3251	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
41	40	ad2ant2l 756	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))
42		eliun 4950	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧))
43		pweq 4566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
44	43	ineq2d 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑓 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ((𝐹‘𝑥) ∩ 𝒫 𝑓))
45	44	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
46	45	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑓 → (∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
47	42, 46	bitrid 285	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑓 → (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)))
48	47	rspcev 3580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 ∈ (𝐺‘𝑘) ∧ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
49	39, 41, 48	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
50		eliun 4950	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
51	49, 50	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
52		simpll 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝜑)
53		simprll 788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
54		fvssunirn 6892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐺‘𝑘) ⊆ ∪ ran 𝐺
55		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = (𝐺‘∅))
56	14	fveq1i 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
57		snex 5393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ {𝑈} ∈ V
58		fr0g 8400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
59	57, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
60	56, 59	eqtri 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐺‘∅) = {𝑈}
61	55, 60	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = ∅ → (𝐺‘𝑛) = {𝑈})
62	61	sseq1d 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = ∅ → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
63		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
64	63	sseq1d 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘𝑘) ⊆ 𝒫 𝑈))
65		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = suc 𝑘 → (𝐺‘𝑛) = (𝐺‘suc 𝑘))
66	65	sseq1d 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑛 = suc 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
67		neibastop2.f	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃))
68		pwidg 4572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ 𝒫 𝑈)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 𝑈 ∈ 𝒫 𝑈)
70	69	snssd 4742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
71		simprl 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
72	67	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹‘𝑃))
73	72	pwexd 5333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
74		inss2 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
75		elpwi 4559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑧 ∈ 𝒫 𝑈 → 𝑧 ⊆ 𝑈)
76	75	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝑧 ⊆ 𝑈)
77	76	sspwd 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
78	74, 77	sstrid 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
79	78	ralrimivw 3157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
80		iunss 4999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
81	79, 80	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
82	81	ralrimiva 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
83		ssralv 4003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
84	83	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
85	82, 84	mpan9 514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
86		iunss 4999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
87	85, 86	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
88	73, 87	ssexd 5277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V)
89		iuneq1 4963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = 𝑎 → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
90		iuneq1 4963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑦 = (𝐺‘𝑘) → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
91	14, 89, 90	frsucmpt2 8404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ω ∧ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
92	71, 88, 91	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
93	92, 87	eqsstrd 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
94	93	expr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ ω) → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
95	94	expcom 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ω → (𝜑 → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
96	62, 64, 66, 70, 95	finds2 7873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ⊆ 𝒫 𝑈))
97		fvex 6874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐺‘𝑛) ∈ V
98	97	elpw 4556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺‘𝑛) ⊆ 𝒫 𝑈)
99	96, 98	imbitrrdi 254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
100	99	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑛 ∈ ω → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
101	100	ralrimiv 3152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
102		ffnfv 7094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈))
103	16, 102	mpbiran 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)
104	101, 103	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐺:ω⟶𝒫 𝒫 𝑈)
105	104	frnd 6694	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
106		sspwuni 5054	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ↔ ∪ ran 𝐺 ⊆ 𝒫 𝑈)
107	105, 106	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
108	107	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran 𝐺 ⊆ 𝒫 𝑈)
109	54, 108	sstrid 3945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
110	52, 53, 109, 92	syl12anc 847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
111	51, 110	eleqtrrd 2864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
112		peano2 7864	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
113	53, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
114		fnfvelrn 7055	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
115	16, 113, 114	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
116		elunii 4867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ∈ ∪ ran 𝐺)
117	111, 115, 116	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ ran 𝐺)
118	117	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ∈ ∪ ran 𝐺)
119		simprr 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
120		pweq 4566	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
121	120	ineq2d 4170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑣 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑣))
122	121	neeq1d 3015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑣 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅))
123	122	rspcev 3580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑣 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
124	118, 119, 123	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)
125	1	reqabi 3436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
126	38, 124, 125	sylanbrc 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑆)
127	126	expr 460	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → (((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦 ∈ 𝑆))
128	127	ralimdva 3173	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → (∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆))
129	128	impr 458	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
130		dfss3 3923	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ⊆ 𝑆 ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)
131	129, 130	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ⊆ 𝑆)
132		velpw 4557	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝒫 𝑆 ↔ 𝑡 ⊆ 𝑆)
133	131, 132	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
134		inelcm 4416	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝐹‘𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
135	26, 133, 134	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
136	25, 135	rexlimddv 3168	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
137	136	expr 460	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
138	137	exlimdv 1952	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
139	19, 138	biimtrid 244	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
140	139	rexlimdvaa 3163	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
141	18, 140	biimtrid 244	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
142	141	rexlimdv 3160	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
143	142	expimpd 457	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144	12, 143	biimtrid 244	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
145	144	ralrimiv 3152	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)
146		pweq 4566	. . . . . . 7 ⊢ (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
147	146	ineq2d 4170	. . . . . 6 ⊢ (𝑜 = 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑆))
148	147	neeq1d 3015	. . . . 5 ⊢ (𝑜 = 𝑆 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
149	148	raleqbi1dv 3329	. . . 4 ⊢ (𝑜 = 𝑆 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
150		neibastop1.4	. . . 4 ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}
151	149, 150	elrab2 3652	. . 3 ⊢ (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))
152	7, 145, 151	sylanbrc 592	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝐽)
153		neibastop2.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
154		snidg 4616	. . . . . 6 ⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ {𝑈})
155	67, 154	syl 17	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ {𝑈})
156		peano1 7863	. . . . . . 7 ⊢ ∅ ∈ ω
157		fnfvelrn 7055	. . . . . . 7 ⊢ ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
158	16, 156, 157	mp2an 702	. . . . . 6 ⊢ (𝐺‘∅) ∈ ran 𝐺
159	60, 158	eqeltrri 2858	. . . . 5 ⊢ {𝑈} ∈ ran 𝐺
160		elunii 4867	. . . . 5 ⊢ ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ∈ ∪ ran 𝐺)
161	155, 159, 160	sylancl 595	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ∪ ran 𝐺)
162		inelcm 4416	. . . . 5 ⊢ ((𝑈 ∈ (𝐹‘𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
163	67, 69, 162	syl2anc 593	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)
164		pweq 4566	. . . . . . 7 ⊢ (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
165	164	ineq2d 4170	. . . . . 6 ⊢ (𝑓 = 𝑈 → ((𝐹‘𝑃) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑈))
166	165	neeq1d 3015	. . . . 5 ⊢ (𝑓 = 𝑈 → (((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅))
167	166	rspcev 3580	. . . 4 ⊢ ((𝑈 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
168	161, 163, 167	syl2anc 593	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)
169		fveq2 6861	. . . . . . 7 ⊢ (𝑦 = 𝑃 → (𝐹‘𝑦) = (𝐹‘𝑃))
170	169	ineq1d 4169	. . . . . 6 ⊢ (𝑦 = 𝑃 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑓))
171	170	neeq1d 3015	. . . . 5 ⊢ (𝑦 = 𝑃 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
172	171	rexbidv 3185	. . . 4 ⊢ (𝑦 = 𝑃 → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
173	172, 1	elrab2 3652	. . 3 ⊢ (𝑃 ∈ 𝑆 ↔ (𝑃 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅))
174	153, 168, 173	sylanbrc 592	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑆)
175		eluni2 4866	. . . . . . 7 ⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧)
176		eleq2 2850	. . . . . . . . . 10 ⊢ (𝑧 = (𝐺‘𝑘) → (𝑓 ∈ 𝑧 ↔ 𝑓 ∈ (𝐺‘𝑘)))
177	176	rexrn 7062	. . . . . . . . 9 ⊢ (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)))
178	16, 177	ax-mp 5	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))
179	104	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
180	179	ffvelcdmda 7059	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ∈ 𝒫 𝒫 𝑈)
181	180	elpwid 4561	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ⊆ 𝒫 𝑈)
182	181	sselda 3934	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → 𝑓 ∈ 𝒫 𝑈)
183	182	adantrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
184	183	elpwid 4561	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑈)
185		neibastop2.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ⊆ 𝑁)
186	185	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈 ⊆ 𝑁)
187	184, 186	sstrd 3944	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑁)
188		n0 4303	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓))
189		elin 3918	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
190		simprrr 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
191	190	elpwid 4561	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ⊆ 𝑓)
192		simpllr 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑋)
193		neibastop1.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
194	193	expr 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
195	194	ralrimiva 3153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
196	195	ad3antrrr 740	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣))
197		simprrl 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹‘𝑦))
198		fveq2 6861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
199	198	eleq2d 2847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ (𝐹‘𝑥) ↔ 𝑣 ∈ (𝐹‘𝑦)))
200		elequ1 2148	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
201	199, 200	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) ↔ (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
202	201	rspcv 3576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) → (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣)))
203	192, 196, 197, 202	syl3c 66	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑣)
204	191, 203	sseldd 3935	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑓)
205	204	expr 460	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → ((𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
206	189, 205	biimtrid 244	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
207	206	exlimdv 1952	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓))
208	188, 207	biimtrid 244	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑓))
209	208	impr 458	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑓)
210	187, 209	sseldd 3935	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑁)
211	210	exp32 424	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
212	211	rexlimdva 3162	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
213	178, 212	biimtrid 244	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
214	175, 213	biimtrid 244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑓 ∈ ∪ ran 𝐺 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)))
215	214	rexlimdv 3160	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))
216	215	3impia 1129	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦 ∈ 𝑁)
217	216	rabssdv 4025	. . 3 ⊢ (𝜑 → {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
218	1, 217	eqsstrid 3972	. 2 ⊢ (𝜑 → 𝑆 ⊆ 𝑁)
219		eleq2 2850	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ 𝑆))
220		sseq1 3959	. . . 4 ⊢ (𝑢 = 𝑆 → (𝑢 ⊆ 𝑁 ↔ 𝑆 ⊆ 𝑁))
221	219, 220	anbi12d 641	. . 3 ⊢ (𝑢 = 𝑆 → ((𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁) ↔ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)))
222	221	rspcev 3580	. 2 ⊢ ((𝑆 ∈ 𝐽 ∧ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
223	152, 174, 218, 222	syl12anc 847	1 ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ≠ wne 2956  ∀wral 3075  ∃wrex 3085  {crab 3413  Vcvv 3453   ∖ cdif 3899   ∩ cin 3901   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4552  {csn 4579  ∪ cuni 4862  ∪ ciun 4946   ↦ cmpt 5178  ran crn 5644   ↾ cres 5645  suc csuc 6342   Fn wfn 6510  ⟶wf 6511  ‘cfv 6515  ωcom 7840  reccrdg 8373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-om 7841  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374

This theorem is referenced by:  neibastop2  36681