Step | Hyp | Ref
| Expression |
1 | | fbasrn.c |
. . 3
⊢ 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) |
2 | | simpl2 1065 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → 𝐹:𝑋⟶𝑌) |
3 | | imassrn 5477 |
. . . . . . . 8
⊢ (𝐹 “ 𝑥) ⊆ ran 𝐹 |
4 | | frn 6053 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝑌 → ran 𝐹 ⊆ 𝑌) |
5 | 3, 4 | syl5ss 3614 |
. . . . . . 7
⊢ (𝐹:𝑋⟶𝑌 → (𝐹 “ 𝑥) ⊆ 𝑌) |
6 | 2, 5 | syl 17 |
. . . . . 6
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ⊆ 𝑌) |
7 | | simpl3 1066 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → 𝑌 ∈ 𝑉) |
8 | | elpw2g 4827 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑉 → ((𝐹 “ 𝑥) ∈ 𝒫 𝑌 ↔ (𝐹 “ 𝑥) ⊆ 𝑌)) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → ((𝐹 “ 𝑥) ∈ 𝒫 𝑌 ↔ (𝐹 “ 𝑥) ⊆ 𝑌)) |
10 | 6, 9 | mpbird 247 |
. . . . 5
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ∈ 𝒫 𝑌) |
11 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) |
12 | 10, 11 | fmptd 6385 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)):𝐵⟶𝒫 𝑌) |
13 | | frn 6053 |
. . . 4
⊢ ((𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)):𝐵⟶𝒫 𝑌 → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
15 | 1, 14 | syl5eqss 3649 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ⊆ 𝒫 𝑌) |
16 | 1 | a1i 11 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
17 | | ffun 6048 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹) |
18 | 17 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → Fun 𝐹) |
19 | | funimaexg 5975 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ 𝐵) → (𝐹 “ 𝑥) ∈ V) |
20 | 19 | ralrimiva 2966 |
. . . . . . 7
⊢ (Fun
𝐹 → ∀𝑥 ∈ 𝐵 (𝐹 “ 𝑥) ∈ V) |
21 | | dmmptg 5632 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 (𝐹 “ 𝑥) ∈ V → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = 𝐵) |
22 | 18, 20, 21 | 3syl 18 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = 𝐵) |
23 | | fbasne0 21634 |
. . . . . . 7
⊢ (𝐵 ∈ (fBas‘𝑋) → 𝐵 ≠ ∅) |
24 | 23 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐵 ≠ ∅) |
25 | 22, 24 | eqnetrd 2861 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
26 | | dm0rn0 5342 |
. . . . . 6
⊢ (dom
(𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = ∅ ↔ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = ∅) |
27 | 26 | necon3bii 2846 |
. . . . 5
⊢ (dom
(𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅ ↔ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
28 | 25, 27 | sylib 208 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ≠ ∅) |
29 | 16, 28 | eqnetrd 2861 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ≠ ∅) |
30 | | fbelss 21637 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑥 ∈ 𝐵) → 𝑥 ⊆ 𝑋) |
31 | 30 | ex 450 |
. . . . . . . 8
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋)) |
32 | 31 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋)) |
33 | | 0nelfb 21635 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (fBas‘𝑋) → ¬ ∅ ∈
𝐵) |
34 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐵 ↔ ∅ ∈ 𝐵)) |
35 | 34 | notbid 308 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (¬ 𝑥 ∈ 𝐵 ↔ ¬ ∅ ∈ 𝐵)) |
36 | 33, 35 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 = ∅ → ¬ 𝑥 ∈ 𝐵)) |
37 | 36 | con2d 129 |
. . . . . . . 8
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅)) |
38 | 37 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅)) |
39 | 32, 38 | jcad 555 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅))) |
40 | | fdm 6051 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
41 | 40 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → dom 𝐹 = 𝑋) |
42 | 41 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ⊆ dom 𝐹 ↔ 𝑥 ⊆ 𝑋)) |
43 | 42 | biimpar 502 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ dom 𝐹) |
44 | | sseqin2 3817 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑥) = 𝑥) |
45 | 43, 44 | sylib 208 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑥) = 𝑥) |
46 | 45 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → ((dom 𝐹 ∩ 𝑥) = ∅ ↔ 𝑥 = ∅)) |
47 | 46 | biimpd 219 |
. . . . . . . . 9
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → ((dom 𝐹 ∩ 𝑥) = ∅ → 𝑥 = ∅)) |
48 | 47 | con3d 148 |
. . . . . . . 8
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 = ∅ → ¬ (dom 𝐹 ∩ 𝑥) = ∅)) |
49 | 48 | expimpd 629 |
. . . . . . 7
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅) → ¬ (dom 𝐹 ∩ 𝑥) = ∅)) |
50 | | eqcom 2629 |
. . . . . . . . 9
⊢ (∅
= (𝐹 “ 𝑥) ↔ (𝐹 “ 𝑥) = ∅) |
51 | | imadisj 5484 |
. . . . . . . . 9
⊢ ((𝐹 “ 𝑥) = ∅ ↔ (dom 𝐹 ∩ 𝑥) = ∅) |
52 | 50, 51 | bitri 264 |
. . . . . . . 8
⊢ (∅
= (𝐹 “ 𝑥) ↔ (dom 𝐹 ∩ 𝑥) = ∅) |
53 | 52 | notbii 310 |
. . . . . . 7
⊢ (¬
∅ = (𝐹 “ 𝑥) ↔ ¬ (dom 𝐹 ∩ 𝑥) = ∅) |
54 | 49, 53 | syl6ibr 242 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅) → ¬ ∅ = (𝐹 “ 𝑥))) |
55 | 39, 54 | syld 47 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐵 → ¬ ∅ = (𝐹 “ 𝑥))) |
56 | 55 | ralrimiv 2965 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∀𝑥 ∈ 𝐵 ¬ ∅ = (𝐹 “ 𝑥)) |
57 | 1 | eleq2i 2693 |
. . . . . . 7
⊢ (∅
∈ 𝐶 ↔ ∅
∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
58 | | 0ex 4790 |
. . . . . . . 8
⊢ ∅
∈ V |
59 | 11 | elrnmpt 5372 |
. . . . . . . 8
⊢ (∅
∈ V → (∅ ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥))) |
60 | 58, 59 | ax-mp 5 |
. . . . . . 7
⊢ (∅
∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
61 | 57, 60 | bitri 264 |
. . . . . 6
⊢ (∅
∈ 𝐶 ↔
∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
62 | 61 | notbii 310 |
. . . . 5
⊢ (¬
∅ ∈ 𝐶 ↔
¬ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
63 | | df-nel 2898 |
. . . . 5
⊢ (∅
∉ 𝐶 ↔ ¬
∅ ∈ 𝐶) |
64 | | ralnex 2992 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 ¬ ∅ = (𝐹 “ 𝑥) ↔ ¬ ∃𝑥 ∈ 𝐵 ∅ = (𝐹 “ 𝑥)) |
65 | 62, 63, 64 | 3bitr4i 292 |
. . . 4
⊢ (∅
∉ 𝐶 ↔
∀𝑥 ∈ 𝐵 ¬ ∅ = (𝐹 “ 𝑥)) |
66 | 56, 65 | sylibr 224 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∅ ∉ 𝐶) |
67 | 1 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝐶 ↔ 𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
68 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑟 ∈ V |
69 | | imaeq2 5462 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐹 “ 𝑥) = (𝐹 “ 𝑢)) |
70 | 69 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑢 ∈ 𝐵 ↦ (𝐹 “ 𝑢)) |
71 | 70 | elrnmpt 5372 |
. . . . . . . . 9
⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢))) |
72 | 68, 71 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢)) |
73 | 67, 72 | bitri 264 |
. . . . . . 7
⊢ (𝑟 ∈ 𝐶 ↔ ∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢)) |
74 | 1 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝐶 ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
75 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
76 | | imaeq2 5462 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝐹 “ 𝑥) = (𝐹 “ 𝑣)) |
77 | 76 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) = (𝑣 ∈ 𝐵 ↦ (𝐹 “ 𝑣)) |
78 | 77 | elrnmpt 5372 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
79 | 75, 78 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣)) |
80 | 74, 79 | bitri 264 |
. . . . . . 7
⊢ (𝑠 ∈ 𝐶 ↔ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣)) |
81 | 73, 80 | anbi12i 733 |
. . . . . 6
⊢ ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) ↔ (∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
82 | | reeanv 3107 |
. . . . . 6
⊢
(∃𝑢 ∈
𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐵 𝑟 = (𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐵 𝑠 = (𝐹 “ 𝑣))) |
83 | 81, 82 | bitr4i 267 |
. . . . 5
⊢ ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) ↔ ∃𝑢 ∈ 𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) |
84 | | fbasssin 21640 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
85 | 84 | 3expb 1266 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
86 | 85 | 3ad2antl1 1223 |
. . . . . . . . 9
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
87 | 86 | adantrr 753 |
. . . . . . . 8
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) → ∃𝑤 ∈ 𝐵 𝑤 ⊆ (𝑢 ∩ 𝑣)) |
88 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ 𝑤) = (𝐹 “ 𝑤) |
89 | | imaeq2 5462 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝐹 “ 𝑥) = (𝐹 “ 𝑤)) |
90 | 89 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → ((𝐹 “ 𝑤) = (𝐹 “ 𝑥) ↔ (𝐹 “ 𝑤) = (𝐹 “ 𝑤))) |
91 | 90 | rspcev 3309 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ 𝐵 ∧ (𝐹 “ 𝑤) = (𝐹 “ 𝑤)) → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
92 | 88, 91 | mpan2 707 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
93 | 92 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥)) |
94 | 1 | eleq2i 2693 |
. . . . . . . . . . . . 13
⊢ ((𝐹 “ 𝑤) ∈ 𝐶 ↔ (𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))) |
95 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
96 | 95 | funimaex 5976 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (𝐹 “ 𝑤) ∈ V) |
97 | 11 | elrnmpt 5372 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑤) ∈ V → ((𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
98 | 18, 96, 97 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝐹 “ 𝑤) ∈ ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
99 | 94, 98 | syl5bb 272 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝐹 “ 𝑤) ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
100 | 99 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ((𝐹 “ 𝑤) ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑤) = (𝐹 “ 𝑥))) |
101 | 93, 100 | mpbird 247 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ∈ 𝐶) |
102 | | imass2 5501 |
. . . . . . . . . . . 12
⊢ (𝑤 ⊆ (𝑢 ∩ 𝑣) → (𝐹 “ 𝑤) ⊆ (𝐹 “ (𝑢 ∩ 𝑣))) |
103 | 102 | ad2antll 765 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ (𝑢 ∩ 𝑣))) |
104 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢 |
105 | | imass2 5501 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝑣) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑢)) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑢) |
107 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑣 |
108 | | imass2 5501 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝑣) ⊆ 𝑣 → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑣)) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝐹 “ 𝑣) |
110 | 106, 109 | ssini 3836 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣)) |
111 | | ineq12 3809 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → (𝑟 ∩ 𝑠) = ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣))) |
112 | 111 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝑟 ∩ 𝑠) = ((𝐹 “ 𝑢) ∩ (𝐹 “ 𝑣))) |
113 | 110, 112 | syl5sseqr 3654 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) |
114 | 103, 113 | sstrd 3613 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠)) |
115 | | sseq1 3626 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹 “ 𝑤) → (𝑧 ⊆ (𝑟 ∩ 𝑠) ↔ (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠))) |
116 | 115 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝐹 “ 𝑤) ∈ 𝐶 ∧ (𝐹 “ 𝑤) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
117 | 101, 114,
116 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
118 | 117 | adantlrl 756 |
. . . . . . . 8
⊢ ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ (𝑢 ∩ 𝑣))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
119 | 87, 118 | rexlimddv 3035 |
. . . . . . 7
⊢ (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)))) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
120 | 119 | exp32 631 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ((𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)))) |
121 | 120 | rexlimdvv 3037 |
. . . . 5
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (∃𝑢 ∈ 𝐵 ∃𝑣 ∈ 𝐵 (𝑟 = (𝐹 “ 𝑢) ∧ 𝑠 = (𝐹 “ 𝑣)) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
122 | 83, 121 | syl5bi 232 |
. . . 4
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ((𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶) → ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
123 | 122 | ralrimivv 2970 |
. . 3
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠)) |
124 | 29, 66, 123 | 3jca 1242 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))) |
125 | | isfbas2 21639 |
. . 3
⊢ (𝑌 ∈ 𝑉 → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))))) |
126 | 125 | 3ad2ant3 1084 |
. 2
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟 ∈ 𝐶 ∀𝑠 ∈ 𝐶 ∃𝑧 ∈ 𝐶 𝑧 ⊆ (𝑟 ∩ 𝑠))))) |
127 | 15, 124, 126 | mpbir2and 957 |
1
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ∈ (fBas‘𝑌)) |