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 22807

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 22797	. . 3 ⊢ (𝐽 ∈ 2^ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
2		omex 9579	. . . . . . 7 ⊢ ω ∈ V
3	2	brdom 8900	. . . . . 6 ⊢ (𝑏 ≼ ω ↔ ∃𝑓 𝑓:𝑏–1-1→ω)
4		ssrab2 4037	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ran 𝑓
5		f1f 6738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏⟶ω)
6	5	frnd 6676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑏–1-1→ω → ran 𝑓 ⊆ ω)
7	6	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ran 𝑓 ⊆ ω)
8	4, 7	sstrid 3955	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
9	8	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
10		eldifsn 4747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ (𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅))
11		n0 4306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
12		tg2 22315	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))
13		omsson 7806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ω ⊆ On
14	8, 13	sstrdi 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
15	14	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
16		f1fn 6739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑏–1-1→ω → 𝑓 Fn 𝑏)
17	16	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓 Fn 𝑏)
18		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝑏)
19		fnfvelrn 7031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn 𝑏 ∧ 𝑧 ∈ 𝑏) → (𝑓‘𝑧) ∈ ran 𝑓)
20	17, 18, 19	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (𝑓‘𝑧) ∈ ran 𝑓)
21		f1f1orn 6795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏–1-1-onto→ran 𝑓)
22	21	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓:𝑏–1-1-onto→ran 𝑓)
23		f1ocnvfv1 7222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓:𝑏–1-1-onto→ran 𝑓 ∧ 𝑧 ∈ 𝑏) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
24	22, 18, 23	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
25		simprrr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ⊆ 𝐵)
26		velpw 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵)
27	25, 26	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝒫 𝐵)
28		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑦 ∈ 𝑧)
29	28	ne0d 4295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ≠ ∅)
30		eldifsn 4747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝒫 𝐵 ∖ {∅}) ↔ (𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ≠ ∅))
31	27, 29, 30	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ (𝒫 𝐵 ∖ {∅}))
32	24, 31	eqeltrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅}))
33		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = (𝑓‘𝑧) → (^◡𝑓‘𝑛) = (^◡𝑓‘(𝑓‘𝑧)))
34	33	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = (𝑓‘𝑧) → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})))
35	34	rspcev 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓‘𝑧) ∈ ran 𝑓 ∧ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
36	20, 32, 35	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
37		rabn0 4345	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅ ↔ ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
38	36, 37	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅)
39		onint 7725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On ∧ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
40	15, 38, 39	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
41	40	rexlimdvaa 3153	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
42	12, 41	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
43	42	expdimp 453	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
44	43	exlimdv 1936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (∃𝑦 𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
45	11, 44	biimtrid 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝐵 ≠ ∅ → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
46	45	expimpd 454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
47	10, 46	biimtrid 241	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
48	47	impr 455	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
49	9, 48	sseldd 3945	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
50	49	expr 457	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
51	50	ralimdva 3164	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
52	51	imp 407	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
53	52	adantrr 715	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
54		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
55	54	fmpt 7058	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω ↔ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
56	53, 55	sylib 217	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
57		neeq1 3006	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝑓‘𝑧) = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → ((^◡𝑓‘𝑧) ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
58		neeq1 3006	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_o = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → (1_o ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
59		1n0 8434	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_o ≠ ∅
60	57, 58, 59	elimhyp 4551	. . . . . . . . . . . . . . . . . 18 ⊢ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅
61		n0 4306	. . . . . . . . . . . . . . . . . 18 ⊢ (if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o))
62	60, 61	mpbi 229	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)
63		19.29r 1877	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
64	62, 63	mpan 688	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
65		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
66	48, 65	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
67	66	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
68		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = 𝑧 → (^◡𝑓‘𝑛) = (^◡𝑓‘𝑧))
69	68	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑧 → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
70	69	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ (𝑧 ∈ ran 𝑓 ∧ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
71	70	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
72	67, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
73		eldifsn 4747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}) ↔ ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
74	72, 73	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
75	74	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ≠ ∅)
76	75	iftrued 4494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) = (^◡𝑓‘𝑧))
77	74	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ 𝒫 𝐵)
78	77	elpwid 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ⊆ 𝐵)
79	76, 78	eqsstrd 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ⊆ 𝐵)
80	79	sseld 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))
81	80	exp31 420	. . . . . . . . . . . . . . . . . . . . . . . . . 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 432	. . . . . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
86	85	ralimdva 3164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
87	86	imp 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
88	87	an32s 650	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
89		rmoim 3698	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
91	90	expimpd 454	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ((𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
92	91	exlimdv 1936	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
93	64, 92	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
94	93	impr 455	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
95		nfcv 2907	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑤
96		nfmpt1 5213	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
97		nfcv 2907	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑧
98	95, 96, 97	nfbr 5152	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧
99		nfv 1917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
100		breq1 5108	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ 𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
101		df-br 5106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
102		df-mpt 5189	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})}
103	102	eleq2i 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) ↔ ⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})})
104		opabidw 5481	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})} ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
105	101, 103, 104	3bitri 296	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
106	100, 105	bitrdi 286	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})))
107	98, 99, 106	cbvmow 2601	. . . . . . . . . . . . . . 15 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
108		df-rmo 3353	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
109	107, 108	bitr4i 277	. . . . . . . . . . . . . 14 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
110	94, 109	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
111	110	alrimiv 1930	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑧∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
112		dff12 6737	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω ↔ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω ∧ ∀𝑧∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
113	56, 111, 112	sylanbrc 583	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω)
114		f1domg 8912	. . . . . . . . . . 11 ⊢ (ω ∈ V → ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω → 𝐴 ≼ ω))
115	2, 113, 114	mpsyl 68	. . . . . . . . . 10 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → 𝐴 ≼ ω)
116	115	ex 413	. . . . . . . . 9 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
117		difeq1 4075	. . . . . . . . . . . . 13 ⊢ ((topGen‘𝑏) = 𝐽 → ((topGen‘𝑏) ∖ {∅}) = (𝐽 ∖ {∅}))
118	117	eleq2d 2823	. . . . . . . . . . . 12 ⊢ ((topGen‘𝑏) = 𝐽 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ 𝐵 ∈ (𝐽 ∖ {∅})))
119	118	ralbidv 3174	. . . . . . . . . . 11 ⊢ ((topGen‘𝑏) = 𝐽 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅})))
120	119	anbi1d 630	. . . . . . . . . 10 ⊢ ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)))
121	120	imbi1d 341	. . . . . . . . 9 ⊢ ((topGen‘𝑏) = 𝐽 → (((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) ↔ ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
122	116, 121	syl5ibcom 244	. . . . . . . 8 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
123	122	ex 413	. . . . . . 7 ⊢ (𝑏 ∈ TopBases → (𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
124	123	exlimdv 1936	. . . . . 6 ⊢ (𝑏 ∈ TopBases → (∃𝑓 𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
125	3, 124	biimtrid 241	. . . . 5 ⊢ (𝑏 ∈ TopBases → (𝑏 ≼ ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
126	125	impd 411	. . . 4 ⊢ (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
127	126	rexlimiv 3145	. . 3 ⊢ (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
128	1, 127	sylbi 216	. 2 ⊢ (𝐽 ∈ 2^ndω → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
129	128	3impib 1116	1 ⊢ ((𝐽 ∈ 2^ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 ∀wal 1539 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ∃*wmo 2536 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 ∃*wrmo 3352 {crab 3407 Vcvv 3445 ∖ cdif 3907 ⊆ wss 3910 ∅c0 4282 ifcif 4486 𝒫 cpw 4560 {csn 4586 ⟨cop 4592 ∩ cint 4907 class class class wbr 5105 {copab 5167 ↦ cmpt 5188 ^◡ccnv 5632 ran crn 5634 Oncon0 6317 Fn wfn 6491 ⟶wf 6492 –1-1→wf1 6493 –1-1-onto→wf1o 6495 ‘cfv 6496 ωcom 7802 1_oc1o 8405 ≼ cdom 8881 topGenctg 17319 TopBasesctb 22295 2^ndωc2ndc 22789

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-om 7803 df-1o 8412 df-dom 8885 df-topgen 17325 df-2ndc 22791

This theorem is referenced by: 2ndcdisj2 22808

W3C validator