Step | Hyp | Ref
| Expression |
1 | | fbasrn.c |
. . 3
⊢ 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) |
2 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → 𝑌 ∈ 𝑉) |
3 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → 𝐹:𝑋⟶𝑌) |
4 | | fimass 6519 |
. . . . . . 7
⊢ (𝐹:𝑋⟶𝑌 → (𝐹 “ 𝑥) ⊆ 𝑌) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ⊆ 𝑌) |
6 | 2, 5 | sselpwd 5191 |
. . . . 5
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ∈ 𝒫 𝑌) |
7 | 6 | fmpttd 6883 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)):𝐵⟶𝒫 𝑌) |
8 | 7 | frnd 6506 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
9 | 1, 8 | eqsstrid 3923 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ⊆ 𝒫 𝑌) |
10 | 1 | a1i 11 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
11 | | ffun 6501 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹) |
12 | 11 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → Fun 𝐹) |
13 | | funimaexg 6419 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ∈ V) |
14 | 13 | ralrimiva 3096 |
. . . . . . 7
⊢ (Fun
𝐹 → ∀𝑥 ∈ 𝐵 (𝐹 “ 𝑥) ∈ V) |
15 | | dmmptg 6068 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 (𝐹 “ 𝑥) ∈ V → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = 𝐵) |
16 | 12, 14, 15 | 3syl 18 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = 𝐵) |
17 | | fbasne0 22574 |
. . . . . . 7
⊢ (𝐵 ∈ (fBas‘𝑋) → 𝐵 ≠ ∅) |
18 | 17 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐵 ≠ ∅) |
19 | 16, 18 | eqnetrd 3001 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
20 | | dm0rn0 5762 |
. . . . . 6
⊢ (dom
(𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = ∅ ↔ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = ∅) |
21 | 20 | necon3bii 2986 |
. . . . 5
⊢ (dom
(𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅ ↔ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
22 | 19, 21 | sylib 221 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
23 | 10, 22 | eqnetrd 3001 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ≠ ∅) |
24 | | fbelss 22577 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑥 ∈ 𝐵) → 𝑥 ⊆ 𝑋) |
25 | 24 | ex 416 |
. . . . . . . 8
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋)) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋)) |
27 | | 0nelfb 22575 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (fBas‘𝑋) → ¬ ∅ ∈
𝐵) |
28 | | eleq1 2820 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐵 ↔ ∅ ∈ 𝐵)) |
29 | 28 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (¬ 𝑥 ∈ 𝐵 ↔ ¬ ∅ ∈ 𝐵)) |
30 | 27, 29 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 = ∅ → ¬ 𝑥 ∈ 𝐵)) |
31 | 30 | con2d 136 |
. . . . . . . 8
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅)) |
32 | 31 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅)) |
33 | 26, 32 | jcad 516 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅))) |
34 | | fdm 6507 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
35 | 34 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom 𝐹 = 𝑋) |
36 | 35 | sseq2d 3907 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ⊆ dom 𝐹 ↔ 𝑥 ⊆ 𝑋)) |
37 | 36 | biimpar 481 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ dom 𝐹) |
38 | | sseqin2 4104 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑥) = 𝑥) |
39 | 37, 38 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑥) = 𝑥) |
40 | 39 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → ((dom 𝐹 ∩ 𝑥) = ∅ ↔ 𝑥 = ∅)) |
41 | 40 | biimpd 232 |
. . . . . . . . 9
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → ((dom 𝐹 ∩ 𝑥) = ∅ → 𝑥 = ∅)) |
42 | 41 | con3d 155 |
. . . . . . . 8
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 = ∅ → ¬ (dom 𝐹 ∩ 𝑥) = ∅)) |
43 | 42 | expimpd 457 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅) → ¬ (dom 𝐹 ∩ 𝑥) = ∅)) |
44 | | eqcom 2745 |
. . . . . . . . 9
⊢ (∅
= (𝐹 “ 𝑥) ↔ (𝐹 “ 𝑥) = ∅) |
45 | | imadisj 5916 |
. . . . . . . . 9
⊢ ((𝐹 “ 𝑥) = ∅ ↔ (dom 𝐹 ∩ 𝑥) = ∅) |
46 | 44, 45 | bitri 278 |
. . . . . . . 8
⊢ (∅
= (𝐹 “ 𝑥) ↔ (dom 𝐹 ∩ 𝑥) = ∅) |
47 | 46 | notbii 323 |
. . . . . . 7
⊢ (¬
∅ = (𝐹 “ 𝑥) ↔ ¬ (dom 𝐹 ∩ 𝑥) = ∅) |
48 | 43, 47 | syl6ibr 255 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅) → ¬ ∅ = (𝐹 “ 𝑥))) |
49 | 33, 48 | syld 47 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → ¬ ∅ = (𝐹 “ 𝑥))) |
50 | 49 | ralrimiv 3095 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∀𝑥 ∈ 𝐵 ¬ ∅ = (𝐹 “ 𝑥)) |
51 | 1 | eleq2i 2824 |
. . . . . . 7
⊢ (∅
∈ 𝐶 ↔ ∅
∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
52 | | 0ex 5172 |
. . . . . . . 8
⊢ ∅
∈ V |
53 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) |
54 | 53 | elrnmpt 5793 |
. . . . . . . 8
⊢ (∅
∈ V → (∅ ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥))) |
55 | 52, 54 | ax-mp 5 |
. . . . . . 7
⊢ (∅
∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
56 | 51, 55 | bitri 278 |
. . . . . 6
⊢ (∅
∈ 𝐶 ↔
∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
57 | 56 | notbii 323 |
. . . . 5
⊢ (¬
∅ ∈ 𝐶 ↔
¬ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
58 | | df-nel 3039 |
. . . . 5
⊢ (∅
∉ 𝐶 ↔ ¬
∅ ∈ 𝐶) |
59 | | ralnex 3148 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 ¬ ∅ = (𝐹 “ 𝑥) ↔ ¬ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
60 | 57, 58, 59 | 3bitr4i 306 |
. . . 4
⊢ (∅
∉ 𝐶 ↔
∀𝑥 ∈ 𝐵 ¬ ∅ = (𝐹 “ 𝑥)) |
61 | 50, 60 | sylibr 237 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∅ ∉ 𝐶) |
62 | 1 | eleq2i 2824 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝐶 ↔ 𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
63 | | imaeq2 5893 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐹 “ 𝑥) = (𝐹 “ 𝑢)) |
64 | 63 | cbvmptv 5130 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑢 ∈ 𝐵 ↦ (𝐹 “ 𝑢)) |
65 | 64 | elrnmpt 5793 |
. . . . . . . . 9
⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢))) |
66 | 65 | elv 3403 |
. . . . . . . 8
⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢)) |
67 | 62, 66 | bitri 278 |
. . . . . . 7
⊢ (𝑟 ∈ 𝐶 ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢)) |
68 | 1 | eleq2i 2824 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝐶 ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
69 | | imaeq2 5893 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝐹 “ 𝑥) = (𝐹 “ 𝑣)) |
70 | 69 | cbvmptv 5130 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑣 ∈ 𝐵 ↦ (𝐹 “ 𝑣)) |
71 | 70 | elrnmpt 5793 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
72 | 71 | elv 3403 |
. . . . . . . 8
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣)) |
73 | 68, 72 | bitri 278 |
. . . . . . 7
⊢ (𝑠 ∈ 𝐶 ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣)) |
74 | 67, 73 | anbi12i 630 |
. . . . . 6
⊢ ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) ↔ (∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
75 | | reeanv 3269 |
. . . . . 6
⊢
(∃𝑢 ∈
𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
76 | 74, 75 | bitr4i 281 |
. . . . 5
⊢ ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) ↔ ∃𝑢 ∈ 𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) |
77 | | fbasssin 22580 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
78 | 77 | 3expb 1121 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
79 | 78 | 3ad2antl1 1186 |
. . . . . . . . 9
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
80 | 79 | adantrr 717 |
. . . . . . . 8
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
81 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ 𝑤) = (𝐹 “ 𝑤) |
82 | | imaeq2 5893 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝐹 “ 𝑥) = (𝐹 “ 𝑤)) |
83 | 82 | rspceeqv 3539 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ 𝐵 ∧ (𝐹 “ 𝑤) = (𝐹 “ 𝑤)) → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
84 | 81, 83 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
85 | 84 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
86 | 1 | eleq2i 2824 |
. . . . . . . . . . . . 13
⊢ ((𝐹 “ 𝑤) ∈ 𝐶 ↔ (𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
87 | | vex 3401 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
88 | 87 | funimaex 6420 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (𝐹 “ 𝑤) ∈ V) |
89 | 53 | elrnmpt 5793 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑤) ∈ V → ((𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
90 | 12, 88, 89 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
91 | 86, 90 | syl5bb 286 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝐹 “ 𝑤) ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
92 | 91 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ((𝐹 “ 𝑤) ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
93 | 85, 92 | mpbird 260 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ∈ 𝐶) |
94 | | imass2 5933 |
. . . . . . . . . . . 12
⊢ (𝑤 ⊆ (𝑢 ∩ 𝑣) → (𝐹 “ 𝑤) ⊆ (𝐹 “ (𝑢 ∩ 𝑣))) |
95 | 94 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ (𝑢 ∩ 𝑣))) |
96 | | inss1 4117 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢 |
97 | | imass2 5933 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝑣) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑢)) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑢) |
99 | | inss2 4118 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑣 |
100 | | imass2 5933 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝑣) ⊆ 𝑣 → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑣)) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑣) |
102 | 98, 101 | ssini 4120 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣)) |
103 | | ineq12 4096 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → (𝑟 ∩ 𝑠) = ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣))) |
104 | 103 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝑟 ∩ 𝑠) = ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣))) |
105 | 102, 104 | sseqtrrid 3928 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) |
106 | 95, 105 | sstrd 3885 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠)) |
107 | | sseq1 3900 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹 “ 𝑤) → (𝑧 ⊆ (𝑟 ∩ 𝑠) ↔ (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠))) |
108 | 107 | rspcev 3524 |
. . . . . . . . . 10
⊢ (((𝐹 “ 𝑤) ∈ 𝐶 ∧ (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
109 | 93, 106, 108 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
110 | 109 | adantlrl 720 |
. . . . . . . 8
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
111 | 80, 110 | rexlimddv 3200 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
112 | 111 | exp32 424 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ((𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)))) |
113 | 112 | rexlimdvv 3202 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (∃𝑢 ∈ 𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
114 | 76, 113 | syl5bi 245 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
115 | 114 | ralrimivv 3102 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
116 | 23, 61, 115 | 3jca 1129 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
117 | | isfbas2 22579 |
. . 3
⊢ (𝑌 ∈ 𝑉 → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))))) |
118 | 117 | 3ad2ant3 1136 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))))) |
119 | 9, 116, 118 | mpbir2and 713 |
1
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ∈ (fBas‘𝑌)) |