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 23582

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 23572	. . 3 ⊢ (𝐽 ∈ 2^ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
2		omex 9612	. . . . . . 7 ⊢ ω ∈ V
3	2	brdom 8957	. . . . . 6 ⊢ (𝑏 ≼ ω ↔ ∃𝑓 𝑓:𝑏–1-1→ω)
4		ssrab2 4042	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ran 𝑓
5		f1f 6775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏⟶ω)
6	5	frnd 6715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑏–1-1→ω → ran 𝑓 ⊆ ω)
7	6	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ran 𝑓 ⊆ ω)
8	4, 7	sstrid 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
9	8	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
10		eldifsn 4758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ (𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅))
11		n0 4315	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
12		tg2 23091	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))
13		omsson 7866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ω ⊆ On
14	8, 13	sstrdi 3957	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
15	14	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
16		f1fn 6776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑏–1-1→ω → 𝑓 Fn 𝑏)
17	16	ad3antlr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓 Fn 𝑏)
18		simprl 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝑏)
19		fnfvelrn 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn 𝑏 ∧ 𝑧 ∈ 𝑏) → (𝑓‘𝑧) ∈ ran 𝑓)
20	17, 18, 19	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (𝑓‘𝑧) ∈ ran 𝑓)
21		f1f1orn 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏–1-1-onto→ran 𝑓)
22	21	ad3antlr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓:𝑏–1-1-onto→ran 𝑓)
23		f1ocnvfv1 7275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓:𝑏–1-1-onto→ran 𝑓 ∧ 𝑧 ∈ 𝑏) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
24	22, 18, 23	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
25		simprrr 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ⊆ 𝐵)
26		velpw 4572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵)
27	25, 26	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝒫 𝐵)
28		simprrl 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑦 ∈ 𝑧)
29	28	ne0d 4303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ≠ ∅)
30		eldifsn 4758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝒫 𝐵 ∖ {∅}) ↔ (𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ≠ ∅))
31	27, 29, 30	sylanbrc 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ (𝒫 𝐵 ∖ {∅}))
32	24, 31	eqeltrd 2869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅}))
33		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = (𝑓‘𝑧) → (^◡𝑓‘𝑛) = (^◡𝑓‘(𝑓‘𝑧)))
34	33	eleq1d 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = (𝑓‘𝑧) → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})))
35	34	rspcev 3590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓‘𝑧) ∈ ran 𝑓 ∧ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
36	20, 32, 35	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
37		rabn0 4353	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅ ↔ ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
38	36, 37	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅)
39		onint 7789	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On ∧ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
40	15, 38, 39	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
41	40	rexlimdvaa 3173	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
42	12, 41	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
43	42	expdimp 457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
44	43	exlimdv 1960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (∃𝑦 𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
45	11, 44	biimtrid 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝐵 ≠ ∅ → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
46	45	expimpd 458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
47	10, 46	biimtrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
48	47	impr 459	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
49	9, 48	sseldd 3946	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
50	49	expr 461	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
51	50	ralimdva 3183	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
52	51	imp 411	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
53	52	adantrr 729	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
54		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
55	54	fmpt 7106	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω ↔ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
56	53, 55	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
57		neeq1 3026	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝑓‘𝑧) = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → ((^◡𝑓‘𝑧) ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
58		neeq1 3026	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_o = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → (1_o ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
59		1n0 8472	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_o ≠ ∅
60	57, 58, 59	elimhyp 4558	. . . . . . . . . . . . . . . . . 18 ⊢ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅
61		n0 4315	. . . . . . . . . . . . . . . . . 18 ⊢ (if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o))
62	60, 61	mpbi 233	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)
63		19.29r 1901	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
64	62, 63	mpan 702	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
65		eleq1 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
66	48, 65	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
67	66	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
68		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = 𝑧 → (^◡𝑓‘𝑛) = (^◡𝑓‘𝑧))
69	68	eleq1d 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑧 → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
70	69	elrab 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ (𝑧 ∈ ran 𝑓 ∧ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
71	70	simprbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
72	67, 71	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
73		eldifsn 4758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}) ↔ ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
74	72, 73	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
75	74	simprd 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ≠ ∅)
76	75	iftrued 4500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) = (^◡𝑓‘𝑧))
77	74	simpld 499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ 𝒫 𝐵)
78	77	elpwid 4576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ⊆ 𝐵)
79	76, 78	eqsstrd 3979	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ⊆ 𝐵)
80	79	sseld 3944	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))
81	80	exp31 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))))
82	81	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))))
83	82	exp4a 436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑥 ∈ 𝐴 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵)))))
84	83	com25 100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → (𝑥 ∈ 𝐴 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))))
85	84	imp31 422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
86	85	ralimdva 3183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
87	86	imp 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
88	87	an32s 664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
89		rmoim 3712	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
90	88, 89	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
91	90	expimpd 458	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ((𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
92	91	exlimdv 1960	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
93	64, 92	syl5 35	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
94	93	impr 459	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
95		nfcv 2931	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑤
96		nfmpt1 5214	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
97		nfcv 2931	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑧
98	95, 96, 97	nfbr 5162	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧
99		nfv 1941	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
100		breq1 5116	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ 𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
101		df-br 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
102		df-mpt 5197	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})}
103	102	eleq2i 2861	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) ↔ ⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})})
104		opabidw 5509	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})} ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
105	101, 103, 104	3bitri 300	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
106	100, 105	bitrdi 290	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})))
107	98, 99, 106	cbvmow 2637	. . . . . . . . . . . . . . 15 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
108		df-rmo 3376	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
109	107, 108	bitr4i 281	. . . . . . . . . . . . . 14 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
110	94, 109	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
111	110	alrimiv 1954	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑧∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
112		dff12 6774	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω ↔ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω ∧ ∀𝑧∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
113	56, 111, 112	sylanbrc 594	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω)
114		f1domg 8968	. . . . . . . . . . 11 ⊢ (ω ∈ V → ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω → 𝐴 ≼ ω))
115	2, 113, 114	mpsyl 69	. . . . . . . . . 10 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → 𝐴 ≼ ω)
116	115	ex 417	. . . . . . . . 9 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
117		difeq1 4082	. . . . . . . . . . . . 13 ⊢ ((topGen‘𝑏) = 𝐽 → ((topGen‘𝑏) ∖ {∅}) = (𝐽 ∖ {∅}))
118	117	eleq2d 2855	. . . . . . . . . . . 12 ⊢ ((topGen‘𝑏) = 𝐽 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ 𝐵 ∈ (𝐽 ∖ {∅})))
119	118	ralbidv 3194	. . . . . . . . . . 11 ⊢ ((topGen‘𝑏) = 𝐽 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅})))
120	119	anbi1d 642	. . . . . . . . . 10 ⊢ ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)))
121	120	imbi1d 344	. . . . . . . . 9 ⊢ ((topGen‘𝑏) = 𝐽 → (((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) ↔ ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
122	116, 121	syl5ibcom 248	. . . . . . . 8 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
123	122	ex 417	. . . . . . 7 ⊢ (𝑏 ∈ TopBases → (𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
124	123	exlimdv 1960	. . . . . 6 ⊢ (𝑏 ∈ TopBases → (∃𝑓 𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
125	3, 124	biimtrid 245	. . . . 5 ⊢ (𝑏 ∈ TopBases → (𝑏 ≼ ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
126	125	impd 415	. . . 4 ⊢ (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
127	126	rexlimiv 3165	. . 3 ⊢ (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
128	1, 127	sylbi 220	. 2 ⊢ (𝐽 ∈ 2^ndω → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
129	128	3impib 1132	1 ⊢ ((𝐽 ∈ 2^ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 ∀wal 1565 = wceq 1567 ∃wex 1806 ∈ wcel 2149 ∃*wmo 2571 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 ∃*wrmo 3375 {crab 3423 Vcvv 3463 ∖ cdif 3910 ⊆ wss 3913 ∅c0 4294 ifcif 4492 𝒫 cpw 4567 {csn 4594 ⟨cop 4600 ∩ cint 4916 class class class wbr 5113 {copab 5177 ↦ cmpt 5196 ^◡ccnv 5661 ran crn 5663 Oncon0 6361 Fn wfn 6532 ⟶wf 6533 –1-1→wf1 6534 –1-1-onto→wf1o 6536 ‘cfv 6537 ωcom 7862 1_oc1o 8446 ≼ cdom 8941 topGenctg 17490 TopBasesctb 23071 2^ndωc2ndc 23564

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9610

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-om 7863 df-1o 8453 df-dom 8945 df-topgen 17496 df-2ndc 23566

This theorem is referenced by: 2ndcdisj2 23583

W3C validator