Step | Hyp | Ref
| Expression |
1 | | fbasrn.c |
. . 3
⊢ 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) |
2 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → 𝐹:𝑋⟶𝑌) |
3 | | imassrn 5396 |
. . . . . . . 8
⊢ (𝐹 “ 𝑥) ⊆ ran 𝐹 |
4 | | frn 5966 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝑌 → ran 𝐹 ⊆ 𝑌) |
5 | 3, 4 | syl5ss 3579 |
. . . . . . 7
⊢ (𝐹:𝑋⟶𝑌 → (𝐹 “ 𝑥) ⊆ 𝑌) |
6 | 2, 5 | syl 17 |
. . . . . 6
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ⊆ 𝑌) |
7 | | simpl3 1059 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → 𝑌 ∈ 𝑉) |
8 | | elpw2g 4754 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑉 → ((𝐹 “ 𝑥) ∈ 𝒫 𝑌 ↔ (𝐹 “ 𝑥) ⊆ 𝑌)) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → ((𝐹 “ 𝑥) ∈ 𝒫 𝑌 ↔ (𝐹 “ 𝑥) ⊆ 𝑌)) |
10 | 6, 9 | mpbird 246 |
. . . . 5
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ∈ 𝒫 𝑌) |
11 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) |
12 | 10, 11 | fmptd 6292 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)):𝐵⟶𝒫 𝑌) |
13 | | frn 5966 |
. . . 4
⊢ ((𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)):𝐵⟶𝒫 𝑌 → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
15 | 1, 14 | syl5eqss 3612 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ⊆ 𝒫 𝑌) |
16 | 1 | a1i 11 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
17 | | ffun 5961 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹) |
18 | 17 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → Fun 𝐹) |
19 | | funimaexg 5889 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ∈ V) |
20 | 19 | ralrimiva 2949 |
. . . . . . 7
⊢ (Fun
𝐹 → ∀𝑥 ∈ 𝐵 (𝐹 “ 𝑥) ∈ V) |
21 | | dmmptg 5549 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 (𝐹 “ 𝑥) ∈ V → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = 𝐵) |
22 | 18, 20, 21 | 3syl 18 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = 𝐵) |
23 | | fbasne0 21444 |
. . . . . . 7
⊢ (𝐵 ∈ (fBas‘𝑋) → 𝐵 ≠ ∅) |
24 | 23 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐵 ≠ ∅) |
25 | 22, 24 | eqnetrd 2849 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
26 | | dm0rn0 5263 |
. . . . . 6
⊢ (dom
(𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = ∅ ↔ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = ∅) |
27 | 26 | necon3bii 2834 |
. . . . 5
⊢ (dom
(𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅ ↔ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
28 | 25, 27 | sylib 207 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
29 | 16, 28 | eqnetrd 2849 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ≠ ∅) |
30 | | fbelss 21447 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑥 ∈ 𝐵) → 𝑥 ⊆ 𝑋) |
31 | 30 | ex 449 |
. . . . . . . 8
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋)) |
32 | 31 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋)) |
33 | | 0nelfb 21445 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (fBas‘𝑋) → ¬ ∅ ∈
𝐵) |
34 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐵 ↔ ∅ ∈ 𝐵)) |
35 | 34 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (¬ 𝑥 ∈ 𝐵 ↔ ¬ ∅ ∈ 𝐵)) |
36 | 33, 35 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 = ∅ → ¬ 𝑥 ∈ 𝐵)) |
37 | 36 | con2d 128 |
. . . . . . . 8
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅)) |
38 | 37 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅)) |
39 | 32, 38 | jcad 554 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅))) |
40 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
41 | 40 | 3ad2ant2 1076 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom 𝐹 = 𝑋) |
42 | 41 | sseq2d 3596 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ⊆ dom 𝐹 ↔ 𝑥 ⊆ 𝑋)) |
43 | 42 | biimpar 501 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ dom 𝐹) |
44 | | sseqin2 3779 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑥) = 𝑥) |
45 | 43, 44 | sylib 207 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑥) = 𝑥) |
46 | 45 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → ((dom 𝐹 ∩ 𝑥) = ∅ ↔ 𝑥 = ∅)) |
47 | 46 | biimpd 218 |
. . . . . . . . 9
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → ((dom 𝐹 ∩ 𝑥) = ∅ → 𝑥 = ∅)) |
48 | 47 | con3d 147 |
. . . . . . . 8
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 = ∅ → ¬ (dom 𝐹 ∩ 𝑥) = ∅)) |
49 | 48 | expimpd 627 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅) → ¬ (dom 𝐹 ∩ 𝑥) = ∅)) |
50 | | eqcom 2617 |
. . . . . . . . 9
⊢ (∅
= (𝐹 “ 𝑥) ↔ (𝐹 “ 𝑥) = ∅) |
51 | | imadisj 5403 |
. . . . . . . . 9
⊢ ((𝐹 “ 𝑥) = ∅ ↔ (dom 𝐹 ∩ 𝑥) = ∅) |
52 | 50, 51 | bitri 263 |
. . . . . . . 8
⊢ (∅
= (𝐹 “ 𝑥) ↔ (dom 𝐹 ∩ 𝑥) = ∅) |
53 | 52 | notbii 309 |
. . . . . . 7
⊢ (¬
∅ = (𝐹 “ 𝑥) ↔ ¬ (dom 𝐹 ∩ 𝑥) = ∅) |
54 | 49, 53 | syl6ibr 241 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅) → ¬ ∅ = (𝐹 “ 𝑥))) |
55 | 39, 54 | syld 46 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → ¬ ∅ = (𝐹 “ 𝑥))) |
56 | 55 | ralrimiv 2948 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∀𝑥 ∈ 𝐵 ¬ ∅ = (𝐹 “ 𝑥)) |
57 | 1 | eleq2i 2680 |
. . . . . . 7
⊢ (∅
∈ 𝐶 ↔ ∅
∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
58 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
59 | 11 | elrnmpt 5293 |
. . . . . . . 8
⊢ (∅
∈ V → (∅ ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥))) |
60 | 58, 59 | ax-mp 5 |
. . . . . . 7
⊢ (∅
∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
61 | 57, 60 | bitri 263 |
. . . . . 6
⊢ (∅
∈ 𝐶 ↔
∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
62 | 61 | notbii 309 |
. . . . 5
⊢ (¬
∅ ∈ 𝐶 ↔
¬ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
63 | | df-nel 2783 |
. . . . 5
⊢ (∅
∉ 𝐶 ↔ ¬
∅ ∈ 𝐶) |
64 | | ralnex 2975 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 ¬ ∅ = (𝐹 “ 𝑥) ↔ ¬ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
65 | 62, 63, 64 | 3bitr4i 291 |
. . . 4
⊢ (∅
∉ 𝐶 ↔
∀𝑥 ∈ 𝐵 ¬ ∅ = (𝐹 “ 𝑥)) |
66 | 56, 65 | sylibr 223 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∅ ∉ 𝐶) |
67 | 1 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝐶 ↔ 𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
68 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑟 ∈ V |
69 | | imaeq2 5381 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐹 “ 𝑥) = (𝐹 “ 𝑢)) |
70 | 69 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑢 ∈ 𝐵 ↦ (𝐹 “ 𝑢)) |
71 | 70 | elrnmpt 5293 |
. . . . . . . . 9
⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢))) |
72 | 68, 71 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢)) |
73 | 67, 72 | bitri 263 |
. . . . . . 7
⊢ (𝑟 ∈ 𝐶 ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢)) |
74 | 1 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝐶 ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
75 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
76 | | imaeq2 5381 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝐹 “ 𝑥) = (𝐹 “ 𝑣)) |
77 | 76 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑣 ∈ 𝐵 ↦ (𝐹 “ 𝑣)) |
78 | 77 | elrnmpt 5293 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
79 | 75, 78 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣)) |
80 | 74, 79 | bitri 263 |
. . . . . . 7
⊢ (𝑠 ∈ 𝐶 ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣)) |
81 | 73, 80 | anbi12i 729 |
. . . . . 6
⊢ ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) ↔ (∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
82 | | reeanv 3086 |
. . . . . 6
⊢
(∃𝑢 ∈
𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
83 | 81, 82 | bitr4i 266 |
. . . . 5
⊢ ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) ↔ ∃𝑢 ∈ 𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) |
84 | | fbasssin 21450 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
85 | 84 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
86 | 85 | 3ad2antl1 1216 |
. . . . . . . . 9
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
87 | 86 | adantrr 749 |
. . . . . . . 8
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
88 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ 𝑤) = (𝐹 “ 𝑤) |
89 | | imaeq2 5381 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝐹 “ 𝑥) = (𝐹 “ 𝑤)) |
90 | 89 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → ((𝐹 “ 𝑤) = (𝐹 “ 𝑥) ↔ (𝐹 “ 𝑤) = (𝐹 “ 𝑤))) |
91 | 90 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ 𝐵 ∧ (𝐹 “ 𝑤) = (𝐹 “ 𝑤)) → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
92 | 88, 91 | mpan2 703 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
93 | 92 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
94 | 1 | eleq2i 2680 |
. . . . . . . . . . . . 13
⊢ ((𝐹 “ 𝑤) ∈ 𝐶 ↔ (𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
95 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
96 | 95 | funimaex 5890 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (𝐹 “ 𝑤) ∈ V) |
97 | 11 | elrnmpt 5293 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑤) ∈ V → ((𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
98 | 18, 96, 97 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
99 | 94, 98 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝐹 “ 𝑤) ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
100 | 99 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ((𝐹 “ 𝑤) ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
101 | 93, 100 | mpbird 246 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ∈ 𝐶) |
102 | | imass2 5420 |
. . . . . . . . . . . 12
⊢ (𝑤 ⊆ (𝑢 ∩ 𝑣) → (𝐹 “ 𝑤) ⊆ (𝐹 “ (𝑢 ∩ 𝑣))) |
103 | 102 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ (𝑢 ∩ 𝑣))) |
104 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢 |
105 | | imass2 5420 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝑣) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑢)) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑢) |
107 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑣 |
108 | | imass2 5420 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝑣) ⊆ 𝑣 → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑣)) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑣) |
110 | 106, 109 | ssini 3798 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣)) |
111 | | ineq12 3771 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → (𝑟 ∩ 𝑠) = ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣))) |
112 | 111 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝑟 ∩ 𝑠) = ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣))) |
113 | 110, 112 | syl5sseqr 3617 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) |
114 | 103, 113 | sstrd 3578 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠)) |
115 | | sseq1 3589 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹 “ 𝑤) → (𝑧 ⊆ (𝑟 ∩ 𝑠) ↔ (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠))) |
116 | 115 | rspcev 3282 |
. . . . . . . . . 10
⊢ (((𝐹 “ 𝑤) ∈ 𝐶 ∧ (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
117 | 101, 114,
116 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
118 | 117 | adantlrl 752 |
. . . . . . . 8
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
119 | 87, 118 | rexlimddv 3017 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
120 | 119 | exp32 629 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ((𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)))) |
121 | 120 | rexlimdvv 3019 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (∃𝑢 ∈ 𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
122 | 83, 121 | syl5bi 231 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
123 | 122 | ralrimivv 2953 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
124 | 29, 66, 123 | 3jca 1235 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
125 | | isfbas2 21449 |
. . 3
⊢ (𝑌 ∈ 𝑉 → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))))) |
126 | 125 | 3ad2ant3 1077 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))))) |
127 | 15, 124, 126 | mpbir2and 959 |
1
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ∈ (fBas‘𝑌)) |