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 23464

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 23454	. . 3 ⊢ (𝐽 ∈ 2^ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
2		omex 9683	. . . . . . 7 ⊢ ω ∈ V
3	2	brdom 9001	. . . . . 6 ⊢ (𝑏 ≼ ω ↔ ∃𝑓 𝑓:𝑏–1-1→ω)
4		ssrab2 4080	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ran 𝑓
5		f1f 6804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏⟶ω)
6	5	frnd 6744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑏–1-1→ω → ran 𝑓 ⊆ ω)
7	6	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ran 𝑓 ⊆ ω)
8	4, 7	sstrid 3995	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
9	8	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
10		eldifsn 4786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ (𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅))
11		n0 4353	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
12		tg2 22972	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))
13		omsson 7891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ω ⊆ On
14	8, 13	sstrdi 3996	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
15	14	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
16		f1fn 6805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑏–1-1→ω → 𝑓 Fn 𝑏)
17	16	ad3antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓 Fn 𝑏)
18		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝑏)
19		fnfvelrn 7100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn 𝑏 ∧ 𝑧 ∈ 𝑏) → (𝑓‘𝑧) ∈ ran 𝑓)
20	17, 18, 19	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (𝑓‘𝑧) ∈ ran 𝑓)
21		f1f1orn 6859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏–1-1-onto→ran 𝑓)
22	21	ad3antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓:𝑏–1-1-onto→ran 𝑓)
23		f1ocnvfv1 7296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓:𝑏–1-1-onto→ran 𝑓 ∧ 𝑧 ∈ 𝑏) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
24	22, 18, 23	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
25		simprrr 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ⊆ 𝐵)
26		velpw 4605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵)
27	25, 26	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝒫 𝐵)
28		simprrl 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑦 ∈ 𝑧)
29	28	ne0d 4342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ≠ ∅)
30		eldifsn 4786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝒫 𝐵 ∖ {∅}) ↔ (𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ≠ ∅))
31	27, 29, 30	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ (𝒫 𝐵 ∖ {∅}))
32	24, 31	eqeltrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅}))
33		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = (𝑓‘𝑧) → (^◡𝑓‘𝑛) = (^◡𝑓‘(𝑓‘𝑧)))
34	33	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = (𝑓‘𝑧) → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})))
35	34	rspcev 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓‘𝑧) ∈ ran 𝑓 ∧ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
36	20, 32, 35	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
37		rabn0 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅ ↔ ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
38	36, 37	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅)
39		onint 7810	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On ∧ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
40	15, 38, 39	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
41	40	rexlimdvaa 3156	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
42	12, 41	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
43	42	expdimp 452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
44	43	exlimdv 1933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (∃𝑦 𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
45	11, 44	biimtrid 242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝐵 ≠ ∅ → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
46	45	expimpd 453	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
47	10, 46	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
48	47	impr 454	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
49	9, 48	sseldd 3984	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
50	49	expr 456	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
51	50	ralimdva 3167	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
52	51	imp 406	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
53	52	adantrr 717	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
54		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
55	54	fmpt 7130	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω ↔ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
56	53, 55	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
57		neeq1 3003	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝑓‘𝑧) = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → ((^◡𝑓‘𝑧) ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
58		neeq1 3003	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_o = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → (1_o ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
59		1n0 8526	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_o ≠ ∅
60	57, 58, 59	elimhyp 4591	. . . . . . . . . . . . . . . . . 18 ⊢ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅
61		n0 4353	. . . . . . . . . . . . . . . . . 18 ⊢ (if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o))
62	60, 61	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)
63		19.29r 1874	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
64	62, 63	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
65		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
66	48, 65	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
67	66	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
68		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = 𝑧 → (^◡𝑓‘𝑛) = (^◡𝑓‘𝑧))
69	68	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑧 → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
70	69	elrab 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ (𝑧 ∈ ran 𝑓 ∧ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
71	70	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
72	67, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
73		eldifsn 4786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}) ↔ ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
74	72, 73	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
75	74	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ≠ ∅)
76	75	iftrued 4533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) = (^◡𝑓‘𝑧))
77	74	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ 𝒫 𝐵)
78	77	elpwid 4609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ⊆ 𝐵)
79	76, 78	eqsstrd 4018	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ⊆ 𝐵)
80	79	sseld 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))
81	80	exp31 419	. . . . . . . . . . . . . . . . . . . . . . . . . 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 431	. . . . . . . . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
86	85	ralimdva 3167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
87	86	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
88	87	an32s 652	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
89		rmoim 3746	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
91	90	expimpd 453	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ((𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
92	91	exlimdv 1933	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
93	64, 92	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
94	93	impr 454	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
95		nfcv 2905	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑤
96		nfmpt1 5250	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
97		nfcv 2905	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑧
98	95, 96, 97	nfbr 5190	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧
99		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
100		breq1 5146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ 𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
101		df-br 5144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
102		df-mpt 5226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})}
103	102	eleq2i 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) ↔ ⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})})
104		opabidw 5529	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})} ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
105	101, 103, 104	3bitri 297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
106	100, 105	bitrdi 287	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})))
107	98, 99, 106	cbvmow 2603	. . . . . . . . . . . . . . 15 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
108		df-rmo 3380	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
109	107, 108	bitr4i 278	. . . . . . . . . . . . . 14 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
110	94, 109	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
111	110	alrimiv 1927	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑧∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
112		dff12 6803	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω ↔ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω ∧ ∀𝑧∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
113	56, 111, 112	sylanbrc 583	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω)
114		f1domg 9012	. . . . . . . . . . 11 ⊢ (ω ∈ V → ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω → 𝐴 ≼ ω))
115	2, 113, 114	mpsyl 68	. . . . . . . . . 10 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → 𝐴 ≼ ω)
116	115	ex 412	. . . . . . . . 9 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
117		difeq1 4119	. . . . . . . . . . . . 13 ⊢ ((topGen‘𝑏) = 𝐽 → ((topGen‘𝑏) ∖ {∅}) = (𝐽 ∖ {∅}))
118	117	eleq2d 2827	. . . . . . . . . . . 12 ⊢ ((topGen‘𝑏) = 𝐽 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ 𝐵 ∈ (𝐽 ∖ {∅})))
119	118	ralbidv 3178	. . . . . . . . . . 11 ⊢ ((topGen‘𝑏) = 𝐽 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅})))
120	119	anbi1d 631	. . . . . . . . . 10 ⊢ ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)))
121	120	imbi1d 341	. . . . . . . . 9 ⊢ ((topGen‘𝑏) = 𝐽 → (((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) ↔ ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
122	116, 121	syl5ibcom 245	. . . . . . . 8 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
123	122	ex 412	. . . . . . 7 ⊢ (𝑏 ∈ TopBases → (𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
124	123	exlimdv 1933	. . . . . 6 ⊢ (𝑏 ∈ TopBases → (∃𝑓 𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
125	3, 124	biimtrid 242	. . . . 5 ⊢ (𝑏 ∈ TopBases → (𝑏 ≼ ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
126	125	impd 410	. . . 4 ⊢ (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
127	126	rexlimiv 3148	. . 3 ⊢ (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
128	1, 127	sylbi 217	. 2 ⊢ (𝐽 ∈ 2^ndω → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
129	128	3impib 1117	1 ⊢ ((𝐽 ∈ 2^ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∃*wmo 2538 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∃*wrmo 3379 {crab 3436 Vcvv 3480 ∖ cdif 3948 ⊆ wss 3951 ∅c0 4333 ifcif 4525 𝒫 cpw 4600 {csn 4626 ⟨cop 4632 ∩ cint 4946 class class class wbr 5143 {copab 5205 ↦ cmpt 5225 ^◡ccnv 5684 ran crn 5686 Oncon0 6384 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 –1-1-onto→wf1o 6560 ‘cfv 6561 ωcom 7887 1_oc1o 8499 ≼ cdom 8983 topGenctg 17482 TopBasesctb 22952 2^ndωc2ndc 23446

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-om 7888 df-1o 8506 df-dom 8987 df-topgen 17488 df-2ndc 23448

This theorem is referenced by: 2ndcdisj2 23465

W3C validator