Step | Hyp | Ref
| Expression |
1 | | pwssplit1.y |
. . 3
⊢ 𝑌 = (𝑊 ↑s 𝑈) |
2 | | pwssplit1.z |
. . 3
⊢ 𝑍 = (𝑊 ↑s 𝑉) |
3 | | pwssplit1.b |
. . 3
⊢ 𝐵 = (Base‘𝑌) |
4 | | pwssplit1.c |
. . 3
⊢ 𝐶 = (Base‘𝑍) |
5 | | pwssplit1.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) |
6 | 1, 2, 3, 4, 5 | pwssplit0 18879 |
. 2
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵⟶𝐶) |
7 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑊 ∈ Mnd) |
8 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑈 ∈ 𝑋) |
9 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑉 ⊆ 𝑈) |
10 | 8, 9 | ssexd 4733 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑉 ∈ V) |
11 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑊) =
(Base‘𝑊) |
12 | 2, 11, 4 | pwselbasb 15971 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Mnd ∧ 𝑉 ∈ V) → (𝑎 ∈ 𝐶 ↔ 𝑎:𝑉⟶(Base‘𝑊))) |
13 | 7, 10, 12 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (𝑎 ∈ 𝐶 ↔ 𝑎:𝑉⟶(Base‘𝑊))) |
14 | 13 | biimpa 500 |
. . . . . . 7
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → 𝑎:𝑉⟶(Base‘𝑊)) |
15 | | fvex 6113 |
. . . . . . . . . 10
⊢
(0g‘𝑊) ∈ V |
16 | 15 | fconst 6004 |
. . . . . . . . 9
⊢ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}):(𝑈 ∖ 𝑉)⟶{(0g‘𝑊)} |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}):(𝑈 ∖ 𝑉)⟶{(0g‘𝑊)}) |
18 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → 𝑊 ∈ Mnd) |
19 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑊) = (0g‘𝑊) |
20 | 11, 19 | mndidcl 17131 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Mnd →
(0g‘𝑊)
∈ (Base‘𝑊)) |
21 | 18, 20 | syl 17 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (0g‘𝑊) ∈ (Base‘𝑊)) |
22 | 21 | snssd 4281 |
. . . . . . . 8
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → {(0g‘𝑊)} ⊆ (Base‘𝑊)) |
23 | 17, 22 | fssd 5970 |
. . . . . . 7
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}):(𝑈 ∖ 𝑉)⟶(Base‘𝑊)) |
24 | | disjdif 3992 |
. . . . . . . 8
⊢ (𝑉 ∩ (𝑈 ∖ 𝑉)) = ∅ |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (𝑉 ∩ (𝑈 ∖ 𝑉)) = ∅) |
26 | | fun 5979 |
. . . . . . 7
⊢ (((𝑎:𝑉⟶(Base‘𝑊) ∧ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}):(𝑈 ∖ 𝑉)⟶(Base‘𝑊)) ∧ (𝑉 ∩ (𝑈 ∖ 𝑉)) = ∅) → (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})):(𝑉 ∪ (𝑈 ∖ 𝑉))⟶((Base‘𝑊) ∪ (Base‘𝑊))) |
27 | 14, 23, 25, 26 | syl21anc 1317 |
. . . . . 6
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})):(𝑉 ∪ (𝑈 ∖ 𝑉))⟶((Base‘𝑊) ∪ (Base‘𝑊))) |
28 | | simpl3 1059 |
. . . . . . . 8
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → 𝑉 ⊆ 𝑈) |
29 | | undif 4001 |
. . . . . . . 8
⊢ (𝑉 ⊆ 𝑈 ↔ (𝑉 ∪ (𝑈 ∖ 𝑉)) = 𝑈) |
30 | 28, 29 | sylib 207 |
. . . . . . 7
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (𝑉 ∪ (𝑈 ∖ 𝑉)) = 𝑈) |
31 | | unidm 3718 |
. . . . . . . 8
⊢
((Base‘𝑊)
∪ (Base‘𝑊)) =
(Base‘𝑊) |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((Base‘𝑊) ∪ (Base‘𝑊)) = (Base‘𝑊)) |
33 | 30, 32 | feq23d 5953 |
. . . . . 6
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})):(𝑉 ∪ (𝑈 ∖ 𝑉))⟶((Base‘𝑊) ∪ (Base‘𝑊)) ↔ (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})):𝑈⟶(Base‘𝑊))) |
34 | 27, 33 | mpbid 221 |
. . . . 5
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})):𝑈⟶(Base‘𝑊)) |
35 | | simpl2 1058 |
. . . . . 6
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → 𝑈 ∈ 𝑋) |
36 | 1, 11, 3 | pwselbasb 15971 |
. . . . . 6
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋) → ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ∈ 𝐵 ↔ (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})):𝑈⟶(Base‘𝑊))) |
37 | 18, 35, 36 | syl2anc 691 |
. . . . 5
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ∈ 𝐵 ↔ (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})):𝑈⟶(Base‘𝑊))) |
38 | 34, 37 | mpbird 246 |
. . . 4
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ∈ 𝐵) |
39 | 5 | fvtresfn 6193 |
. . . . . 6
⊢ ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ∈ 𝐵 → (𝐹‘(𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}))) = ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ↾ 𝑉)) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (𝐹‘(𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}))) = ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ↾ 𝑉)) |
41 | | resundir 5331 |
. . . . . . 7
⊢ ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ↾ 𝑉) = ((𝑎 ↾ 𝑉) ∪ (((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) ↾ 𝑉)) |
42 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑎:𝑉⟶(Base‘𝑊) → 𝑎 Fn 𝑉) |
43 | | fnresdm 5914 |
. . . . . . . . 9
⊢ (𝑎 Fn 𝑉 → (𝑎 ↾ 𝑉) = 𝑎) |
44 | 14, 42, 43 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (𝑎 ↾ 𝑉) = 𝑎) |
45 | | incom 3767 |
. . . . . . . . . 10
⊢ ((𝑈 ∖ 𝑉) ∩ 𝑉) = (𝑉 ∩ (𝑈 ∖ 𝑉)) |
46 | 45, 24 | eqtri 2632 |
. . . . . . . . 9
⊢ ((𝑈 ∖ 𝑉) ∩ 𝑉) = ∅ |
47 | | fnconstg 6006 |
. . . . . . . . . . 11
⊢
((0g‘𝑊) ∈ V → ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) Fn (𝑈 ∖ 𝑉)) |
48 | 15, 47 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) Fn (𝑈 ∖ 𝑉) |
49 | | fnresdisj 5915 |
. . . . . . . . . 10
⊢ (((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) Fn (𝑈 ∖ 𝑉) → (((𝑈 ∖ 𝑉) ∩ 𝑉) = ∅ ↔ (((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) ↾ 𝑉) = ∅)) |
50 | 48, 49 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (((𝑈 ∖ 𝑉) ∩ 𝑉) = ∅ ↔ (((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) ↾ 𝑉) = ∅)) |
51 | 46, 50 | mpbii 222 |
. . . . . . . 8
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → (((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) ↾ 𝑉) = ∅) |
52 | 44, 51 | uneq12d 3730 |
. . . . . . 7
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((𝑎 ↾ 𝑉) ∪ (((𝑈 ∖ 𝑉) × {(0g‘𝑊)}) ↾ 𝑉)) = (𝑎 ∪ ∅)) |
53 | 41, 52 | syl5eq 2656 |
. . . . . 6
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ↾ 𝑉) = (𝑎 ∪ ∅)) |
54 | | un0 3919 |
. . . . . 6
⊢ (𝑎 ∪ ∅) = 𝑎 |
55 | 53, 54 | syl6eq 2660 |
. . . . 5
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ↾ 𝑉) = 𝑎) |
56 | 40, 55 | eqtr2d 2645 |
. . . 4
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → 𝑎 = (𝐹‘(𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})))) |
57 | | fveq2 6103 |
. . . . . 6
⊢ (𝑏 = (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) → (𝐹‘𝑏) = (𝐹‘(𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})))) |
58 | 57 | eqeq2d 2620 |
. . . . 5
⊢ (𝑏 = (𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) → (𝑎 = (𝐹‘𝑏) ↔ 𝑎 = (𝐹‘(𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)}))))) |
59 | 58 | rspcev 3282 |
. . . 4
⊢ (((𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})) ∈ 𝐵 ∧ 𝑎 = (𝐹‘(𝑎 ∪ ((𝑈 ∖ 𝑉) × {(0g‘𝑊)})))) → ∃𝑏 ∈ 𝐵 𝑎 = (𝐹‘𝑏)) |
60 | 38, 56, 59 | syl2anc 691 |
. . 3
⊢ (((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ 𝐶) → ∃𝑏 ∈ 𝐵 𝑎 = (𝐹‘𝑏)) |
61 | 60 | ralrimiva 2949 |
. 2
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → ∀𝑎 ∈ 𝐶 ∃𝑏 ∈ 𝐵 𝑎 = (𝐹‘𝑏)) |
62 | | dffo3 6282 |
. 2
⊢ (𝐹:𝐵–onto→𝐶 ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑎 ∈ 𝐶 ∃𝑏 ∈ 𝐵 𝑎 = (𝐹‘𝑏))) |
63 | 6, 61, 62 | sylanbrc 695 |
1
⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵–onto→𝐶) |