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 23830

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 23819	. . 3 ⊢ (𝐽 ∈ 2^ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
2		omex 9681	. . . . . . 7 ⊢ ω ∈ V
3	2	brdom 9025	. . . . . 6 ⊢ (𝑏 ≼ ω ↔ ∃𝑓 𝑓:𝑏⟶1-1ω)
4		ssrab2 4008	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ran 𝑓
5		f1f 6808	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑏⟶1-1ω → 𝑓:𝑏⟶ω)
6	5	frnd 6748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑏⟶1-1ω → ran 𝑓 ⊆ ω)
7	6	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) → ran 𝑓 ⊆ ω)
8	4, 7	sstrid 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
9	8	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ω)
10		eldifsn 4750	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ (𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅))
11		n0 4303	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
12		tg2 23338	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))
13		omsson 7915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ω ⊆ On
14	8, 13	sstrdi 3925	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
15	14	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On)
16		f1fn 6809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑏⟶1-1ω → 𝑓 Fn 𝑏)
17	16	ad3antlr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓 Fn 𝑏)
18		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝑏)
19		fnfvelrn 7112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 Fn 𝑏 ∧ 𝑧 ∈ 𝑏) → (𝑓‘𝑧) ∈ ran 𝑓)
20	17, 18, 19	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (𝑓‘𝑧) ∈ ran 𝑓)
21		f1f1orn 6866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑏⟶1-1ω → 𝑓:𝑏⟶1-1ontoran 𝑓)
22	21	ad3antlr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓:𝑏⟶1-1ontoran 𝑓)
23		f1ocnvfv1 7315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓:𝑏⟶1-1ontoran 𝑓 ∧ 𝑧 ∈ 𝑏) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
24	22, 18, 23	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) = 𝑧)
25		simprrr 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ⊆ 𝐵)
26		velpw 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵)
27	25, 26	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝒫 𝐵)
28		simprrl 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑦 ∈ 𝑧)
29	28	ne0d 4291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ≠ ∅)
30		eldifsn 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝒫 𝐵 ∖ {∅}) ↔ (𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ≠ ∅))
31	27, 29, 30	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ (𝒫 𝐵 ∖ {∅}))
32	24, 31	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅}))
33		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = (𝑓‘𝑧) → (^◡𝑓‘𝑛) = (^◡𝑓‘(𝑓‘𝑧)))
34	33	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = (𝑓‘𝑧) → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})))
35	34	rspcev 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓‘𝑧) ∈ ran 𝑓 ∧ (^◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
36	20, 32, 35	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
37		rabn0 4342	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅ ↔ ∃𝑛 ∈ ran 𝑓(^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}))
38	36, 37	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅)
39		onint 7838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On ∧ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
40	15, 38, 39	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
41	40	rexlimdvaa 3168	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
42	12, 41	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
43	42	expdimp 458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
44	43	exlimdv 1968	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (∃𝑦 𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
45	11, 44	biimtrid 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝐵 ≠ ∅ → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
46	45	expimpd 459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
47	10, 46	biimtrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
48	47	impr 460	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
49	9, 48	sseldd 3914	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
50	49	expr 462	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
51	50	ralimdva 3178	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω))
52	51	imp 412	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
53	52	adantrr 730	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω)
54		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
55	54	fmpt 7142	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω ↔ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
56	53, 55	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω)
57		neeq1 3021	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝑓‘𝑧) = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → ((^◡𝑓‘𝑧) ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
58		neeq1 3021	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_o = if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → (1_o ≠ ∅ ↔ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅))
59		1n0 8533	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_o ≠ ∅
60	57, 58, 59	elimhyp 4551	. . . . . . . . . . . . . . . . . 18 ⊢ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅
61		n0 4303	. . . . . . . . . . . . . . . . . 18 ⊢ (if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o))
62	60, 61	mpbi 233	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)
63		19.29r 1909	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑦 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
64	62, 63	mpan 703	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
65		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
66	48, 65	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
67	66	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
68		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑛 = 𝑧 → (^◡𝑓‘𝑛) = (^◡𝑓‘𝑧))
69	68	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑛 = 𝑧 → ((^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
70	69	elrab 3648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ (𝑧 ∈ ran 𝑓 ∧ (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})))
71	70	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
72	67, 71	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))
73		eldifsn 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((^◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}) ↔ ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
74	72, 73	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → ((^◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (^◡𝑓‘𝑧) ≠ ∅))
75	74	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ≠ ∅)
76	75	iftrued 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) = (^◡𝑓‘𝑧))
77	74	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ∈ 𝒫 𝐵)
78	77	elpwid 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (^◡𝑓‘𝑧) ⊆ 𝐵)
79	76, 78	eqsstrd 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ⊆ 𝐵)
80	79	sseld 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) → 𝑦 ∈ 𝐵))
81	80	exp31 425	. . . . . . . . . . . . . . . . . . . . . . . . . 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 437	. . . . . . . . . . . . . . . . . . . . . . . 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 423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
86	85	ralimdva 3178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)))
87	86	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
88	87	an32s 665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))
89		rmoim 3701	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
90	88, 89	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
91	90	expimpd 459	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ((𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
92	91	exlimdv 1968	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∃𝑦(𝑦 ∈ if((^◡𝑓‘𝑧) ≠ ∅, (^◡𝑓‘𝑧), 1_o) ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
93	64, 92	syl5 35	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
94	93	impr 460	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
95		nfcv 2926	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑤
96		nfmpt1 5210	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
97		nfcv 2926	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑧
98	95, 96, 97	nfbr 5158	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧
99		nfv 1949	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})
100		breq1 5111	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ 𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
101		df-br 5109	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
102		df-mpt 5193	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})}
103	102	eleq2i 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) ↔ ⟨𝑥, 𝑧⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})})
104		opabidw 5505	. . . . . . . . . . . . . . . . . 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 2631	. . . . . . . . . . . . . . 15 ⊢ (∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))
108		df-rmo 3369	. . . . . . . . . . . . . . 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 1962	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑧∃𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)
112		dff12 6807	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶1-1ω ↔ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω ∧ ∀𝑧∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧))
113	56, 111, 112	sylanbrc 595	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶1-1ω)
114		f1domg 9036	. . . . . . . . . . 11 ⊢ (ω ∈ V → ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (^◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶1-1ω → 𝐴 ≼ ω))
115	2, 113, 114	mpsyl 69	. . . . . . . . . 10 ⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → 𝐴 ≼ ω)
116	115	ex 418	. . . . . . . . 9 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
117		difeq1 4059	. . . . . . . . . . . . 13 ⊢ ((topGen‘𝑏) = 𝐽 → ((topGen‘𝑏) ∖ {∅}) = (𝐽 ∖ {∅}))
118	117	eleq2d 2850	. . . . . . . . . . . 12 ⊢ ((topGen‘𝑏) = 𝐽 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ 𝐵 ∈ (𝐽 ∖ {∅})))
119	118	ralbidv 3189	. . . . . . . . . . 11 ⊢ ((topGen‘𝑏) = 𝐽 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅})))
120	119	anbi1d 643	. . . . . . . . . 10 ⊢ ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)))
121	120	imbi1d 344	. . . . . . . . 9 ⊢ ((topGen‘𝑏) = 𝐽 → (((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) ↔ ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
122	116, 121	syl5ibcom 248	. . . . . . . 8 ⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏⟶1-1ω) → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
123	122	ex 418	. . . . . . 7 ⊢ (𝑏 ∈ TopBases → (𝑓:𝑏⟶1-1ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
124	123	exlimdv 1968	. . . . . 6 ⊢ (𝑏 ∈ TopBases → (∃𝑓 𝑓:𝑏⟶1-1ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
125	3, 124	biimtrid 245	. . . . 5 ⊢ (𝑏 ∈ TopBases → (𝑏 ≼ ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))))
126	125	impd 416	. . . 4 ⊢ (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))
127	126	rexlimiv 3160	. . 3 ⊢ (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
128	1, 127	sylbi 220	. 2 ⊢ (𝐽 ∈ 2^ndω → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))
129	128	3impib 1134	1 ⊢ ((𝐽 ∈ 2^ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ∃*wmo 2565 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 ∃*wrmo 3368 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∅c0 4281 ifcif 4485 𝒫 cpw 4560 {csn 4588 ⟨cop 4840 ∩ cint 4912 class class class wbr 5108 {copab 5173 ↦ cmpt 5192 ^◡ccnv 5657 ran crn 5659 Oncon0 6388 Fn wfn 6561 ⟶wf 6562 ⟶1-1wf1 6563 ⟶1-1ontowf1o 6565 ‘cfv 6566 ωcom 7911 1_oc1o 8507 ≼ cdom 9009 topGenctg 17658 TopBasesctb 23318 2^ndωc2ndc 23811

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-om 7912 df-1o 8514 df-dom 9013 df-topgen 17664 df-2ndc 23813

This theorem is used by: 2ndcdisj2 23831

W3C validator