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

Theorem fbssfi 22363
 Description: A filter base contains subsets of its finite intersections. (Contributed by Mario Carneiro, 26-Nov-2013.) (Revised by Stefan O'Rear, 28-Jul-2015.)
Assertion
Ref Expression
fbssfi ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ (fi‘𝐹)) → ∃𝑥𝐹 𝑥𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝑋

Proof of Theorem fbssfi
Dummy variables 𝑡 𝑢 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dffi2 8879 . . . 4 (𝐹 ∈ (fBas‘𝑋) → (fi‘𝐹) = {𝑧 ∣ (𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧)})
2 sseq2 3996 . . . . . . . . . . . . . . . 16 (𝑡 = (𝑢𝑣) → (𝑥𝑡𝑥 ⊆ (𝑢𝑣)))
32rexbidv 3301 . . . . . . . . . . . . . . 15 (𝑡 = (𝑢𝑣) → (∃𝑥𝐹 𝑥𝑡 ↔ ∃𝑥𝐹 𝑥 ⊆ (𝑢𝑣)))
4 inss1 4208 . . . . . . . . . . . . . . . . 17 (𝑢𝑣) ⊆ 𝑢
5 simp1r 1192 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → 𝑢 ∈ 𝒫 𝐹)
65elpwid 4555 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → 𝑢 𝐹)
74, 6sstrid 3981 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → (𝑢𝑣) ⊆ 𝐹)
8 vex 3502 . . . . . . . . . . . . . . . . . 18 𝑢 ∈ V
98inex1 5217 . . . . . . . . . . . . . . . . 17 (𝑢𝑣) ∈ V
109elpw 4548 . . . . . . . . . . . . . . . 16 ((𝑢𝑣) ∈ 𝒫 𝐹 ↔ (𝑢𝑣) ⊆ 𝐹)
117, 10sylibr 235 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → (𝑢𝑣) ∈ 𝒫 𝐹)
12 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) → 𝐹 ∈ (fBas‘𝑋))
13 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑦𝐹𝑦𝑢) → 𝑦𝐹)
14 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑧𝐹𝑧𝑣) → 𝑧𝐹)
15 fbasssin 22362 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦𝐹𝑧𝐹) → ∃𝑥𝐹 𝑥 ⊆ (𝑦𝑧))
1612, 13, 14, 15syl3an 1154 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → ∃𝑥𝐹 𝑥 ⊆ (𝑦𝑧))
17 ss2in 4216 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑢𝑧𝑣) → (𝑦𝑧) ⊆ (𝑢𝑣))
1817ad2ant2l 742 . . . . . . . . . . . . . . . . . . 19 (((𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → (𝑦𝑧) ⊆ (𝑢𝑣))
19183adant1 1124 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → (𝑦𝑧) ⊆ (𝑢𝑣))
20 sstr 3978 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ⊆ (𝑦𝑧) ∧ (𝑦𝑧) ⊆ (𝑢𝑣)) → 𝑥 ⊆ (𝑢𝑣))
2120expcom 414 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑧) ⊆ (𝑢𝑣) → (𝑥 ⊆ (𝑦𝑧) → 𝑥 ⊆ (𝑢𝑣)))
2219, 21syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → (𝑥 ⊆ (𝑦𝑧) → 𝑥 ⊆ (𝑢𝑣)))
2322reximdv 3277 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → (∃𝑥𝐹 𝑥 ⊆ (𝑦𝑧) → ∃𝑥𝐹 𝑥 ⊆ (𝑢𝑣)))
2416, 23mpd 15 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → ∃𝑥𝐹 𝑥 ⊆ (𝑢𝑣))
253, 11, 24elrabd 3685 . . . . . . . . . . . . . 14 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢) ∧ (𝑧𝐹𝑧𝑣)) → (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
26253expa 1112 . . . . . . . . . . . . 13 ((((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢)) ∧ (𝑧𝐹𝑧𝑣)) → (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
2726rexlimdvaa 3289 . . . . . . . . . . . 12 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢)) → (∃𝑧𝐹 𝑧𝑣 → (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
2827ralrimivw 3187 . . . . . . . . . . 11 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢)) → ∀𝑣 ∈ 𝒫 𝐹(∃𝑧𝐹 𝑧𝑣 → (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
29 sseq2 3996 . . . . . . . . . . . . . 14 (𝑡 = 𝑣 → (𝑥𝑡𝑥𝑣))
3029rexbidv 3301 . . . . . . . . . . . . 13 (𝑡 = 𝑣 → (∃𝑥𝐹 𝑥𝑡 ↔ ∃𝑥𝐹 𝑥𝑣))
31 sseq1 3995 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥𝑣𝑧𝑣))
3231cbvrexvw 3455 . . . . . . . . . . . . 13 (∃𝑥𝐹 𝑥𝑣 ↔ ∃𝑧𝐹 𝑧𝑣)
3330, 32syl6bb 288 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (∃𝑥𝐹 𝑥𝑡 ↔ ∃𝑧𝐹 𝑧𝑣))
3433ralrab 3688 . . . . . . . . . . 11 (∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ↔ ∀𝑣 ∈ 𝒫 𝐹(∃𝑧𝐹 𝑧𝑣 → (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
3528, 34sylibr 235 . . . . . . . . . 10 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) ∧ (𝑦𝐹𝑦𝑢)) → ∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
3635rexlimdvaa 3289 . . . . . . . . 9 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 𝐹) → (∃𝑦𝐹 𝑦𝑢 → ∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
3736ralrimiva 3186 . . . . . . . 8 (𝐹 ∈ (fBas‘𝑋) → ∀𝑢 ∈ 𝒫 𝐹(∃𝑦𝐹 𝑦𝑢 → ∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
38 sseq2 3996 . . . . . . . . . . 11 (𝑡 = 𝑢 → (𝑥𝑡𝑥𝑢))
3938rexbidv 3301 . . . . . . . . . 10 (𝑡 = 𝑢 → (∃𝑥𝐹 𝑥𝑡 ↔ ∃𝑥𝐹 𝑥𝑢))
40 sseq1 3995 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥𝑢𝑦𝑢))
4140cbvrexvw 3455 . . . . . . . . . 10 (∃𝑥𝐹 𝑥𝑢 ↔ ∃𝑦𝐹 𝑦𝑢)
4239, 41syl6bb 288 . . . . . . . . 9 (𝑡 = 𝑢 → (∃𝑥𝐹 𝑥𝑡 ↔ ∃𝑦𝐹 𝑦𝑢))
4342ralrab 3688 . . . . . . . 8 (∀𝑢 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ↔ ∀𝑢 ∈ 𝒫 𝐹(∃𝑦𝐹 𝑦𝑢 → ∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
4437, 43sylibr 235 . . . . . . 7 (𝐹 ∈ (fBas‘𝑋) → ∀𝑢 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
45 pwuni 4872 . . . . . . . 8 𝐹 ⊆ 𝒫 𝐹
46 ssid 3992 . . . . . . . . . 10 𝑡𝑡
47 sseq1 3995 . . . . . . . . . . 11 (𝑥 = 𝑡 → (𝑥𝑡𝑡𝑡))
4847rspcev 3626 . . . . . . . . . 10 ((𝑡𝐹𝑡𝑡) → ∃𝑥𝐹 𝑥𝑡)
4946, 48mpan2 687 . . . . . . . . 9 (𝑡𝐹 → ∃𝑥𝐹 𝑥𝑡)
5049rgen 3152 . . . . . . . 8 𝑡𝐹𝑥𝐹 𝑥𝑡
51 ssrab 4052 . . . . . . . 8 (𝐹 ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ↔ (𝐹 ⊆ 𝒫 𝐹 ∧ ∀𝑡𝐹𝑥𝐹 𝑥𝑡))
5245, 50, 51mpbir2an 707 . . . . . . 7 𝐹 ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}
5344, 52jctil 520 . . . . . 6 (𝐹 ∈ (fBas‘𝑋) → (𝐹 ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
54 uniexg 7460 . . . . . . 7 (𝐹 ∈ (fBas‘𝑋) → 𝐹 ∈ V)
55 pwexg 5275 . . . . . . 7 ( 𝐹 ∈ V → 𝒫 𝐹 ∈ V)
56 rabexg 5230 . . . . . . 7 (𝒫 𝐹 ∈ V → {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∈ V)
57 sseq2 3996 . . . . . . . . 9 (𝑧 = {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} → (𝐹𝑧𝐹 ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
58 eleq2 2905 . . . . . . . . . . 11 (𝑧 = {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} → ((𝑢𝑣) ∈ 𝑧 ↔ (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
5958raleqbi1dv 3408 . . . . . . . . . 10 (𝑧 = {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} → (∀𝑣𝑧 (𝑢𝑣) ∈ 𝑧 ↔ ∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
6059raleqbi1dv 3408 . . . . . . . . 9 (𝑧 = {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} → (∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧 ↔ ∀𝑢 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}))
6157, 60anbi12d 630 . . . . . . . 8 (𝑧 = {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} → ((𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧) ↔ (𝐹 ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})))
6261elabg 3669 . . . . . . 7 ({𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∈ V → ({𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∈ {𝑧 ∣ (𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧)} ↔ (𝐹 ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})))
6354, 55, 56, 624syl 19 . . . . . 6 (𝐹 ∈ (fBas‘𝑋) → ({𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∈ {𝑧 ∣ (𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧)} ↔ (𝐹 ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} (𝑢𝑣) ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})))
6453, 63mpbird 258 . . . . 5 (𝐹 ∈ (fBas‘𝑋) → {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∈ {𝑧 ∣ (𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧)})
65 intss1 4888 . . . . 5 ({𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ∈ {𝑧 ∣ (𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧)} → {𝑧 ∣ (𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧)} ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
6664, 65syl 17 . . . 4 (𝐹 ∈ (fBas‘𝑋) → {𝑧 ∣ (𝐹𝑧 ∧ ∀𝑢𝑧𝑣𝑧 (𝑢𝑣) ∈ 𝑧)} ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
671, 66eqsstrd 4008 . . 3 (𝐹 ∈ (fBas‘𝑋) → (fi‘𝐹) ⊆ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
6867sselda 3970 . 2 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ (fi‘𝐹)) → 𝐴 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡})
69 sseq2 3996 . . . . 5 (𝑡 = 𝐴 → (𝑥𝑡𝑥𝐴))
7069rexbidv 3301 . . . 4 (𝑡 = 𝐴 → (∃𝑥𝐹 𝑥𝑡 ↔ ∃𝑥𝐹 𝑥𝐴))
7170elrab 3683 . . 3 (𝐴 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} ↔ (𝐴 ∈ 𝒫 𝐹 ∧ ∃𝑥𝐹 𝑥𝐴))
7271simprbi 497 . 2 (𝐴 ∈ {𝑡 ∈ 𝒫 𝐹 ∣ ∃𝑥𝐹 𝑥𝑡} → ∃𝑥𝐹 𝑥𝐴)
7368, 72syl 17 1 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ (fi‘𝐹)) → ∃𝑥𝐹 𝑥𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  {cab 2803  ∀wral 3142  ∃wrex 3143  {crab 3146  Vcvv 3499   ∩ cin 3938   ⊆ wss 3939  𝒫 cpw 4541  ∪ cuni 4836  ∩ cint 4873  ‘cfv 6351  ficfi 8866  fBascfbas 20451 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-en 8502  df-fin 8505  df-fi 8867  df-fbas 20460 This theorem is referenced by:  fbssint  22364  fbunfip  22395  fmfnfmlem1  22480  fmfnfmlem4  22483
 Copyright terms: Public domain W3C validator