2ndcdisj - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 2ndcdisj		Structured version Visualization version GIF version

Theorem 2ndcdisj 22066

Description: Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)

**Assertion**
Ref	Expression
2ndcdisj	⊢ ((𝐽 ∈ 2^ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)

Distinct variable groups: 𝑥,𝑦,𝐴 𝑦,𝐵 𝑥,𝐽 Allowed substitution hints: 𝐵(𝑥) 𝐽(𝑦)

Proof of Theorem 2ndcdisj Dummy variables 𝑓 𝑏 𝑤 𝑧 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		is2ndc 22056	. . 3 ⊢ (𝐽 ∈ 2^ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
2		omex 9108	. . . . . . 7 ⊢ ω ∈ V
3	2	brdom 8523	. . . . . 6 ⊢ (𝑏 ≼ ω ↔ ∃𝑓 𝑓:𝑏–1-1→ω)
4		ssrab2 4058	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ran 𝑓
5		f1f 6577	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏⟶ω)
6	5	frnd 6523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑏–1-1→ω → ran 𝑓 ⊆ ω)
7	6	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ran 𝑓 ⊆ ω)
8	4, 7	sstrid 3980	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
9	8	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
10		eldifsn 4721	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ (𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅))
11		n0 4312	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
12		tg2 21575	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))
13		omsson 7586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ω ⊆ On
14	8, 13	sstrdi 3981	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
15	14	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
16		f1fn 6578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑏–1-1→ω → 𝑓 Fn 𝑏)
17	16	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓 Fn 𝑏)
18		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝑏)
19		fnfvelrn 6850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn 𝑏 ∧ 𝑧 ∈ 𝑏) → (𝑓‘𝑧) ∈ ran 𝑓)
20	17, 18, 19	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (𝑓‘𝑧) ∈ ran 𝑓)
21		f1f1orn 6628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏–1-1-onto→ran 𝑓)
22	21	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓:𝑏–1-1-onto→ran 𝑓)
23		f1ocnvfv1 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓:𝑏–1-1-onto→ran 𝑓 ∧ 𝑧 ∈ 𝑏) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
24	22, 18, 23	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
25		simprrr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ⊆ 𝐵)
26		velpw 4546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵)
27	25, 26	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝒫 𝐵)
28		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑦 ∈ 𝑧)
29	28	ne0d 4303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ≠ ∅)
30		eldifsn 4721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝒫 𝐵 ∖ {∅}) ↔ (𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ≠ ∅))
31	27, 29, 30	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ (𝒫 𝐵 ∖ {∅}))
32	24, 31	eqeltrd 2915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅}))
33		fveq2 6672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = (𝑓‘𝑧) → (^◡𝑓‘𝑛) = (^◡𝑓‘(𝑓‘𝑧)))
34	33	eleq1d 2899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = (𝑓‘𝑧) → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})))
35	34	rspcev 3625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓‘𝑧) ∈ ran 𝑓 ∧ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
36	20, 32, 35	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
37		rabn0 4341	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅ ↔ ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
38	36, 37	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅)
39		onint 7512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On ∧ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
40	15, 38, 39	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
41	40	rexlimdvaa 3287	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
42	12, 41	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
43	42	expdimp 455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
44	43	exlimdv 1934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (∃𝑦 𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
45	11, 44	syl5bi 244	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝐵 ≠ ∅ → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
46	45	expimpd 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
47	10, 46	syl5bi 244	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
48	47	impr 457	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
49	9, 48	sseldd 3970	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
50	49	expr 459	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
51	50	ralimdva 3179	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
52	51	imp 409	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
53	52	adantrr 715	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
54		eqid 2823	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
55	54	fmpt 6876	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω ↔ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
56	53, 55	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
57		neeq1 3080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝑓‘𝑧) = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → ((^◡𝑓‘𝑧) ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
58		neeq1 3080	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_o = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → (1_o ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
59		1n0 8121	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_o ≠ ∅
60	57, 58, 59	elimhyp 4532	. . . . . . . . . . . . . . . . . 18 ⊢ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅
61		n0 4312	. . . . . . . . . . . . . . . . . 18 ⊢ (if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o))
62	60, 61	mpbi 232	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)
63		19.29r 1875	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
64	62, 63	mpan 688	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
65		eleq1 2902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
66	48, 65	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
67	66	imp 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
68		fveq2 6672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = 𝑧 → (^◡𝑓‘𝑛) = (^◡𝑓‘𝑧))
69	68	eleq1d 2899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑧 → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
70	69	elrab 3682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ (𝑧 ∈ ran 𝑓 ∧ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
71	70	simprbi 499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
72	67, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
73		eldifsn 4721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}) ↔ ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
74	72, 73	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
75	74	simprd 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ≠ ∅)
76	75	iftrued 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) = (^◡𝑓‘𝑧))
77	74	simpld 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ 𝒫 𝐵)
78	77	elpwid 4552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ⊆ 𝐵)
79	76, 78	eqsstrd 4007	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ⊆ 𝐵)
80	79	sseld 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))
81	80	exp31 422	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))))
82	81	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))))
83	82	exp4a 434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑥 ∈ 𝐴 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵)))))
84	83	com25 99	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → (𝑥 ∈ 𝐴 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))))
85	84	imp31 420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
86	85	ralimdva 3179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
87	86	imp 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
88	87	an32s 650	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
89		rmoim 3733	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
91	90	expimpd 456	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ((𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
92	91	exlimdv 1934	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
93	64, 92	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
94	93	impr 457	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
95		nfcv 2979	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑤
96		nfmpt1 5166	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
97		nfcv 2979	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑧
98	95, 96, 97	nfbr 5115	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧
99		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
100		breq1 5071	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ 𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
101		df-br 5069	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
102		df-mpt 5149	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})}
103	102	eleq2i 2906	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) ↔ ⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})})
104		opabidw 5414	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})} ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
105	101, 103, 104	3bitri 299	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
106	100, 105	syl6bb 289	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})))
107	98, 99, 106	cbvmow 2688	. . . . . . . . . . . . . . 15 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
108		df-rmo 3148	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
109	107, 108	bitr4i 280	. . . . . . . . . . . . . 14 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
110	94, 109	sylibr 236	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
111	110	alrimiv 1928	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑧∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
112		dff12 6576	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω ↔ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω ∧ ∀𝑧∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
113	56, 111, 112	sylanbrc 585	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω)
114		f1domg 8531	. . . . . . . . . . 11 ⊢ (ω ∈ V → ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω → 𝐴 ≼ ω))
115	2, 113, 114	mpsyl 68	. . . . . . . . . 10 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → 𝐴 ≼ ω)
116	115	ex 415	. . . . . . . . 9 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
117		difeq1 4094	. . . . . . . . . . . . 13 ⊢ ((topGen‘𝑏) = 𝐽 → ((topGen‘𝑏) ∖ {∅}) = (𝐽 ∖ {∅}))
118	117	eleq2d 2900	. . . . . . . . . . . 12 ⊢ ((topGen‘𝑏) = 𝐽 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ 𝐵 ∈ (𝐽 ∖ {∅})))
119	118	ralbidv 3199	. . . . . . . . . . 11 ⊢ ((topGen‘𝑏) = 𝐽 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅})))
120	119	anbi1d 631	. . . . . . . . . 10 ⊢ ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)))
121	120	imbi1d 344	. . . . . . . . 9 ⊢ ((topGen‘𝑏) = 𝐽 → (((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) ↔ ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
122	116, 121	syl5ibcom 247	. . . . . . . 8 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
123	122	ex 415	. . . . . . 7 ⊢ (𝑏 ∈ TopBases → (𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
124	123	exlimdv 1934	. . . . . 6 ⊢ (𝑏 ∈ TopBases → (∃𝑓 𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
125	3, 124	syl5bi 244	. . . . 5 ⊢ (𝑏 ∈ TopBases → (𝑏 ≼ ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
126	125	impd 413	. . . 4 ⊢ (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
127	126	rexlimiv 3282	. . 3 ⊢ (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
128	1, 127	sylbi 219	. 2 ⊢ (𝐽 ∈ 2^ndω → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
129	128	3impib 1112	1 ⊢ ((𝐽 ∈ 2^ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 ∀wal 1535 = wceq 1537 ∃wex 1780 ∈ wcel 2114 ∃*wmo 2620 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 ∃*wrmo 3143 {crab 3144 Vcvv 3496 ∖ cdif 3935 ⊆ wss 3938 ∅c0 4293 ifcif 4469 𝒫 cpw 4541 {csn 4569 ⟨cop 4575 ∩ cint 4878 class class class wbr 5068 {copab 5130 ↦ cmpt 5148 ^◡ccnv 5556 ran crn 5558 Oncon0 6193 Fn wfn 6352 ⟶wf 6353 –1-1→wf1 6354 –1-1-onto→wf1o 6356 ‘cfv 6357 ωcom 7582 1_oc1o 8097 ≼ cdom 8509 topGenctg 16713 TopBasesctb 21555 2^ndωc2ndc 22048

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-inf2 9106

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-om 7583 df-1o 8104 df-dom 8513 df-topgen 16719 df-2ndc 22050

This theorem is referenced by: 2ndcdisj2 22067

W3C validator