| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | neibastop2.s | . . . . 5
⊢ 𝑆 = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} | 
| 2 |  | ssrab2 4079 | . . . . 5
⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋 | 
| 3 | 1, 2 | eqsstri 4029 | . . . 4
⊢ 𝑆 ⊆ 𝑋 | 
| 4 |  | neibastop1.1 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 5 |  | elpw2g 5332 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋)) | 
| 6 | 4, 5 | syl 17 | . . . 4
⊢ (𝜑 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋)) | 
| 7 | 3, 6 | mpbiri 258 | . . 3
⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋) | 
| 8 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) | 
| 9 | 8 | ineq1d 4218 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑥) ∩ 𝒫 𝑓)) | 
| 10 | 9 | neeq1d 2999 | . . . . . . 7
⊢ (𝑦 = 𝑥 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅)) | 
| 11 | 10 | rexbidv 3178 | . . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅)) | 
| 12 | 11, 1 | elrab2 3694 | . . . . 5
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅)) | 
| 13 |  | frfnom 8476 | . . . . . . . . . 10
⊢
(rec((𝑎 ∈ V
↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn
ω | 
| 14 |  | neibastop2.g | . . . . . . . . . . 11
⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) | 
| 15 | 14 | fneq1i 6664 | . . . . . . . . . 10
⊢ (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn
ω) | 
| 16 | 13, 15 | mpbir 231 | . . . . . . . . 9
⊢ 𝐺 Fn ω | 
| 17 |  | fnunirn 7275 | . . . . . . . . 9
⊢ (𝐺 Fn ω → (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))) | 
| 18 | 16, 17 | ax-mp 5 | . . . . . . . 8
⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)) | 
| 19 |  | n0 4352 | . . . . . . . . . 10
⊢ (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) | 
| 20 |  | inss1 4236 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹‘𝑥) | 
| 21 | 20 | sseli 3978 | . . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹‘𝑥)) | 
| 22 |  | neibastop1.6 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) | 
| 23 | 22 | anassrs 467 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ (𝐹‘𝑥)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) | 
| 24 | 21, 23 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) | 
| 25 | 24 | adantrl 716 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) | 
| 26 |  | simprl 770 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹‘𝑥)) | 
| 27 |  | fvssunirn 6938 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹‘𝑥) ⊆ ∪ ran
𝐹 | 
| 28 |  | neibastop1.2 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖
{∅})) | 
| 29 | 28 | frnd 6743 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖
{∅})) | 
| 30 | 29 | difss2d 4138 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋) | 
| 31 |  | sspwuni 5099 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ran
𝐹 ⊆ 𝒫
𝒫 𝑋 ↔ ∪ ran 𝐹 ⊆ 𝒫 𝑋) | 
| 32 | 30, 31 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∪ ran 𝐹 ⊆ 𝒫 𝑋) | 
| 33 | 32 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran
𝐹 ⊆ 𝒫 𝑋) | 
| 34 | 27, 33 | sstrid 3994 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐹‘𝑥) ⊆ 𝒫 𝑋) | 
| 35 | 34 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ∈ 𝒫 𝑋) | 
| 36 | 35 | elpwid 4608 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → 𝑡 ⊆ 𝑋) | 
| 37 | 36 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → 𝑦 ∈ 𝑋) | 
| 38 | 37 | adantrr 717 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑋) | 
| 39 |  | simprlr 779 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺‘𝑘)) | 
| 40 |  | rspe 3248 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) | 
| 41 | 40 | ad2ant2l 746 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) | 
| 42 |  | eliun 4994 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 43 |  | pweq 4613 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓) | 
| 44 | 43 | ineq2d 4219 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 = 𝑓 → ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ((𝐹‘𝑥) ∩ 𝒫 𝑓)) | 
| 45 | 44 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) | 
| 46 | 45 | rexbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑓 → (∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) | 
| 47 | 42, 46 | bitrid 283 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑓 → (𝑣 ∈ ∪
𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) | 
| 48 | 47 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 ∈ (𝐺‘𝑘) ∧ ∃𝑥 ∈ 𝑋 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪
𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 49 | 39, 41, 48 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪
𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 50 |  | eliun 4994 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 ∈ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺‘𝑘)𝑣 ∈ ∪
𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 51 | 49, 50 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪
𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 52 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝜑) | 
| 53 |  | simprll 778 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω) | 
| 54 |  | fvssunirn 6938 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐺‘𝑘) ⊆ ∪ ran
𝐺 | 
| 55 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑛 = ∅ → (𝐺‘𝑛) = (𝐺‘∅)) | 
| 56 | 14 | fveq1i 6906 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾
ω)‘∅) | 
| 57 |  | snex 5435 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ {𝑈} ∈ V | 
| 58 |  | fr0g 8477 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}) | 
| 59 | 57, 58 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((rec((𝑎 ∈ V
↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈} | 
| 60 | 56, 59 | eqtri 2764 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝐺‘∅) = {𝑈} | 
| 61 | 55, 60 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑛 = ∅ → (𝐺‘𝑛) = {𝑈}) | 
| 62 | 61 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑛 = ∅ → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈)) | 
| 63 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) | 
| 64 | 63 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) | 
| 65 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑛 = suc 𝑘 → (𝐺‘𝑛) = (𝐺‘suc 𝑘)) | 
| 66 | 65 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑛 = suc 𝑘 → ((𝐺‘𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)) | 
| 67 |  | neibastop2.f | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃)) | 
| 68 |  | pwidg 4619 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ 𝒫 𝑈) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 𝑈 ∈ 𝒫 𝑈) | 
| 70 | 69 | snssd 4808 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → {𝑈} ⊆ 𝒫 𝑈) | 
| 71 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω) | 
| 72 | 67 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹‘𝑃)) | 
| 73 | 72 | pwexd 5378 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V) | 
| 74 |  | inss2 4237 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧 | 
| 75 |  | elpwi 4606 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑧 ∈ 𝒫 𝑈 → 𝑧 ⊆ 𝑈) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝑧 ⊆ 𝑈) | 
| 77 | 76 | sspwd 4612 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈) | 
| 78 | 74, 77 | sstrid 3994 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 79 | 78 | ralrimivw 3149 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 80 |  | iunss 5044 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 81 | 79, 80 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝑈) → ∪
𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 82 | 81 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 83 |  | ssralv 4051 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)) | 
| 84 | 83 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)) | 
| 85 | 82, 84 | mpan9 506 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 86 |  | iunss 5044 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 87 | 85, 86 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈) | 
| 88 | 73, 87 | ssexd 5323 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V) | 
| 89 |  | iuneq1 5007 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 = 𝑎 → ∪
𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 90 |  | iuneq1 5007 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 = (𝐺‘𝑘) → ∪
𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 91 | 14, 89, 90 | frsucmpt2 8481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑘 ∈ ω ∧ ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 92 | 71, 88, 91 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 93 | 92, 87 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺‘𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈) | 
| 94 | 93 | expr 456 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)) | 
| 95 | 94 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑘 ∈ ω → (𝜑 → ((𝐺‘𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))) | 
| 96 | 62, 64, 66, 70, 95 | finds2 7921 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ⊆ 𝒫 𝑈)) | 
| 97 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐺‘𝑛) ∈ V | 
| 98 | 97 | elpw 4603 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺‘𝑛) ⊆ 𝒫 𝑈) | 
| 99 | 96, 98 | imbitrrdi 252 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑛 ∈ ω → (𝜑 → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)) | 
| 100 | 99 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑛 ∈ ω → (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)) | 
| 101 | 100 | ralrimiv 3144 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈) | 
| 102 |  | ffnfv 7138 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐺:ω⟶𝒫
𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈)) | 
| 103 | 16, 102 | mpbiran 709 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐺:ω⟶𝒫
𝒫 𝑈 ↔
∀𝑛 ∈ ω
(𝐺‘𝑛) ∈ 𝒫 𝒫 𝑈) | 
| 104 | 101, 103 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐺:ω⟶𝒫 𝒫 𝑈) | 
| 105 | 104 | frnd 6743 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈) | 
| 106 |  | sspwuni 5099 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ran
𝐺 ⊆ 𝒫
𝒫 𝑈 ↔ ∪ ran 𝐺 ⊆ 𝒫 𝑈) | 
| 107 | 105, 106 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ∪ ran 𝐺 ⊆ 𝒫 𝑈) | 
| 108 | 107 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ∪ ran
𝐺 ⊆ 𝒫 𝑈) | 
| 109 | 54, 108 | sstrid 3994 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘𝑘) ⊆ 𝒫 𝑈) | 
| 110 | 52, 53, 109, 92 | syl12anc 836 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = ∪ 𝑧 ∈ (𝐺‘𝑘)∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) | 
| 111 | 51, 110 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘)) | 
| 112 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) | 
| 113 | 53, 112 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω) | 
| 114 |  | fnfvelrn 7099 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺) | 
| 115 | 16, 113, 114 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺) | 
| 116 |  | elunii 4911 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ∈ ∪ ran
𝐺) | 
| 117 | 111, 115,
116 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ ∪ ran
𝐺) | 
| 118 | 117 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ∈ ∪ ran
𝐺) | 
| 119 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) | 
| 120 |  | pweq 4613 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣) | 
| 121 | 120 | ineq2d 4219 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑣 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑣)) | 
| 122 | 121 | neeq1d 2999 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑣 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) | 
| 123 | 122 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑣 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅) | 
| 124 | 118, 119,
123 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅) | 
| 125 | 1 | reqabi 3459 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) | 
| 126 | 38, 124, 125 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑡 ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦 ∈ 𝑆) | 
| 127 | 126 | expr 456 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑡) → (((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦 ∈ 𝑆)) | 
| 128 | 127 | ralimdva 3166 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹‘𝑥)) → (∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆)) | 
| 129 | 128 | impr 454 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆) | 
| 130 |  | dfss3 3971 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 ⊆ 𝑆 ↔ ∀𝑦 ∈ 𝑡 𝑦 ∈ 𝑆) | 
| 131 | 129, 130 | sylibr 234 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ⊆ 𝑆) | 
| 132 |  | velpw 4604 | . . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝒫 𝑆 ↔ 𝑡 ⊆ 𝑆) | 
| 133 | 131, 132 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆) | 
| 134 |  | inelcm 4464 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (𝐹‘𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅) | 
| 135 | 26, 133, 134 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹‘𝑥) ∧ ∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅) | 
| 136 | 25, 135 | rexlimddv 3160 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘)) ∧ 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓))) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅) | 
| 137 | 136 | expr 456 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 138 | 137 | exlimdv 1932 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑥) ∩ 𝒫 𝑓) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 139 | 19, 138 | biimtrid 242 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺‘𝑘))) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 140 | 139 | rexlimdvaa 3155 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))) | 
| 141 | 18, 140 | biimtrid 242 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 ∈ ∪ ran
𝐺 → (((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅))) | 
| 142 | 141 | rexlimdv 3152 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 143 | 142 | expimpd 453 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 144 | 12, 143 | biimtrid 242 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 145 | 144 | ralrimiv 3144 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅) | 
| 146 |  | pweq 4613 | . . . . . . 7
⊢ (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆) | 
| 147 | 146 | ineq2d 4219 | . . . . . 6
⊢ (𝑜 = 𝑆 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑆)) | 
| 148 | 147 | neeq1d 2999 | . . . . 5
⊢ (𝑜 = 𝑆 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 149 | 148 | raleqbi1dv 3337 | . . . 4
⊢ (𝑜 = 𝑆 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 150 |  | neibastop1.4 | . . . 4
⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅} | 
| 151 | 149, 150 | elrab2 3694 | . . 3
⊢ (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑆 ((𝐹‘𝑥) ∩ 𝒫 𝑆) ≠ ∅)) | 
| 152 | 7, 145, 151 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝑆 ∈ 𝐽) | 
| 153 |  | neibastop2.p | . . 3
⊢ (𝜑 → 𝑃 ∈ 𝑋) | 
| 154 |  | snidg 4659 | . . . . . 6
⊢ (𝑈 ∈ (𝐹‘𝑃) → 𝑈 ∈ {𝑈}) | 
| 155 | 67, 154 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑈 ∈ {𝑈}) | 
| 156 |  | peano1 7911 | . . . . . . 7
⊢ ∅
∈ ω | 
| 157 |  | fnfvelrn 7099 | . . . . . . 7
⊢ ((𝐺 Fn ω ∧ ∅ ∈
ω) → (𝐺‘∅) ∈ ran 𝐺) | 
| 158 | 16, 156, 157 | mp2an 692 | . . . . . 6
⊢ (𝐺‘∅) ∈ ran 𝐺 | 
| 159 | 60, 158 | eqeltrri 2837 | . . . . 5
⊢ {𝑈} ∈ ran 𝐺 | 
| 160 |  | elunii 4911 | . . . . 5
⊢ ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ∈ ∪ ran
𝐺) | 
| 161 | 155, 159,
160 | sylancl 586 | . . . 4
⊢ (𝜑 → 𝑈 ∈ ∪ ran
𝐺) | 
| 162 |  | inelcm 4464 | . . . . 5
⊢ ((𝑈 ∈ (𝐹‘𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅) | 
| 163 | 67, 69, 162 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅) | 
| 164 |  | pweq 4613 | . . . . . . 7
⊢ (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈) | 
| 165 | 164 | ineq2d 4219 | . . . . . 6
⊢ (𝑓 = 𝑈 → ((𝐹‘𝑃) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑈)) | 
| 166 | 165 | neeq1d 2999 | . . . . 5
⊢ (𝑓 = 𝑈 → (((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅)) | 
| 167 | 166 | rspcev 3621 | . . . 4
⊢ ((𝑈 ∈ ∪ ran 𝐺 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅) | 
| 168 | 161, 163,
167 | syl2anc 584 | . . 3
⊢ (𝜑 → ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅) | 
| 169 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝑃 → (𝐹‘𝑦) = (𝐹‘𝑃)) | 
| 170 | 169 | ineq1d 4218 | . . . . . 6
⊢ (𝑦 = 𝑃 → ((𝐹‘𝑦) ∩ 𝒫 𝑓) = ((𝐹‘𝑃) ∩ 𝒫 𝑓)) | 
| 171 | 170 | neeq1d 2999 | . . . . 5
⊢ (𝑦 = 𝑃 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)) | 
| 172 | 171 | rexbidv 3178 | . . . 4
⊢ (𝑦 = 𝑃 → (∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)) | 
| 173 | 172, 1 | elrab2 3694 | . . 3
⊢ (𝑃 ∈ 𝑆 ↔ (𝑃 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑃) ∩ 𝒫 𝑓) ≠ ∅)) | 
| 174 | 153, 168,
173 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝑃 ∈ 𝑆) | 
| 175 |  | eluni2 4910 | . . . . . . 7
⊢ (𝑓 ∈ ∪ ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧) | 
| 176 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (𝑧 = (𝐺‘𝑘) → (𝑓 ∈ 𝑧 ↔ 𝑓 ∈ (𝐺‘𝑘))) | 
| 177 | 176 | rexrn 7106 | . . . . . . . . 9
⊢ (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘))) | 
| 178 | 16, 177 | ax-mp 5 | . . . . . . . 8
⊢
(∃𝑧 ∈ ran
𝐺 𝑓 ∈ 𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘)) | 
| 179 | 104 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈) | 
| 180 | 179 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ∈ 𝒫 𝒫 𝑈) | 
| 181 | 180 | elpwid 4608 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝐺‘𝑘) ⊆ 𝒫 𝑈) | 
| 182 | 181 | sselda 3982 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → 𝑓 ∈ 𝒫 𝑈) | 
| 183 | 182 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈) | 
| 184 | 183 | elpwid 4608 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑈) | 
| 185 |  | neibastop2.u | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ⊆ 𝑁) | 
| 186 | 185 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈 ⊆ 𝑁) | 
| 187 | 184, 186 | sstrd 3993 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ⊆ 𝑁) | 
| 188 |  | n0 4352 | . . . . . . . . . . . . 13
⊢ (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓)) | 
| 189 |  | elin 3966 | . . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓)) | 
| 190 |  | simprrr 781 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓) | 
| 191 | 190 | elpwid 4608 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ⊆ 𝑓) | 
| 192 |  | simpllr 775 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑋) | 
| 193 |  | neibastop1.5 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣) | 
| 194 | 193 | expr 456 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣)) | 
| 195 | 194 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣)) | 
| 196 | 195 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣)) | 
| 197 |  | simprrl 780 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹‘𝑦)) | 
| 198 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) | 
| 199 | 198 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝑣 ∈ (𝐹‘𝑥) ↔ 𝑣 ∈ (𝐹‘𝑦))) | 
| 200 |  | elequ1 2114 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣)) | 
| 201 | 199, 200 | imbi12d 344 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) ↔ (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣))) | 
| 202 | 201 | rspcv 3617 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑣 ∈ (𝐹‘𝑥) → 𝑥 ∈ 𝑣) → (𝑣 ∈ (𝐹‘𝑦) → 𝑦 ∈ 𝑣))) | 
| 203 | 192, 196,
197, 202 | syl3c 66 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑣) | 
| 204 | 191, 203 | sseldd 3983 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ (𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦 ∈ 𝑓) | 
| 205 | 204 | expr 456 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → ((𝑣 ∈ (𝐹‘𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦 ∈ 𝑓)) | 
| 206 | 189, 205 | biimtrid 242 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓)) | 
| 207 | 206 | exlimdv 1932 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹‘𝑦) ∩ 𝒫 𝑓) → 𝑦 ∈ 𝑓)) | 
| 208 | 188, 207 | biimtrid 242 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺‘𝑘)) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑓)) | 
| 209 | 208 | impr 454 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑓) | 
| 210 | 187, 209 | sseldd 3983 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺‘𝑘) ∧ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦 ∈ 𝑁) | 
| 211 | 210 | exp32 420 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))) | 
| 212 | 211 | rexlimdva 3154 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺‘𝑘) → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))) | 
| 213 | 178, 212 | biimtrid 242 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))) | 
| 214 | 175, 213 | biimtrid 242 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑓 ∈ ∪ ran
𝐺 → (((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁))) | 
| 215 | 214 | rexlimdv 3152 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦 ∈ 𝑁)) | 
| 216 | 215 | 3impia 1117 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦 ∈ 𝑁) | 
| 217 | 216 | rabssdv 4074 | . . 3
⊢ (𝜑 → {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran
𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁) | 
| 218 | 1, 217 | eqsstrid 4021 | . 2
⊢ (𝜑 → 𝑆 ⊆ 𝑁) | 
| 219 |  | eleq2 2829 | . . . 4
⊢ (𝑢 = 𝑆 → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ 𝑆)) | 
| 220 |  | sseq1 4008 | . . . 4
⊢ (𝑢 = 𝑆 → (𝑢 ⊆ 𝑁 ↔ 𝑆 ⊆ 𝑁)) | 
| 221 | 219, 220 | anbi12d 632 | . . 3
⊢ (𝑢 = 𝑆 → ((𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁) ↔ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁))) | 
| 222 | 221 | rspcev 3621 | . 2
⊢ ((𝑆 ∈ 𝐽 ∧ (𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁)) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁)) | 
| 223 | 152, 174,
218, 222 | syl12anc 836 | 1
⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁)) |