Step | Hyp | Ref
| Expression |
1 | | resf1o.2 |
. 2
⊢ 𝐹 = (𝑓 ∈ 𝑋 ↦ (𝑓 ↾ 𝐶)) |
2 | | resexg 5442 |
. . 3
⊢ (𝑓 ∈ 𝑋 → (𝑓 ↾ 𝐶) ∈ V) |
3 | 2 | adantl 482 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ 𝑓 ∈ 𝑋) → (𝑓 ↾ 𝐶) ∈ V) |
4 | | simpr 477 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐶)) → 𝑔 ∈ (𝐵 ↑𝑚 𝐶)) |
5 | | difexg 4808 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐶) ∈ V) |
6 | 5 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∖ 𝐶) ∈ V) |
7 | | snex 4908 |
. . . . . 6
⊢ {𝑍} ∈ V |
8 | | xpexg 6960 |
. . . . . 6
⊢ (((𝐴 ∖ 𝐶) ∈ V ∧ {𝑍} ∈ V) → ((𝐴 ∖ 𝐶) × {𝑍}) ∈ V) |
9 | 6, 7, 8 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) → ((𝐴 ∖ 𝐶) × {𝑍}) ∈ V) |
10 | 9 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐶)) → ((𝐴 ∖ 𝐶) × {𝑍}) ∈ V) |
11 | | unexg 6959 |
. . . 4
⊢ ((𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ ((𝐴 ∖ 𝐶) × {𝑍}) ∈ V) → (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})) ∈ V) |
12 | 4, 10, 11 | syl2anc 693 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐶)) → (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})) ∈ V) |
13 | 12 | adantlr 751 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐶)) → (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})) ∈ V) |
14 | | resf1o.1 |
. . . . 5
⊢ 𝑋 = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶} |
15 | 14 | rabeq2i 3197 |
. . . 4
⊢ (𝑓 ∈ 𝑋 ↔ (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶)) |
16 | 15 | anbi1i 731 |
. . 3
⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 = (𝑓 ↾ 𝐶)) ↔ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) |
17 | | simprr 796 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑔 = (𝑓 ↾ 𝐶)) |
18 | | simprll 802 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑓 ∈ (𝐵 ↑𝑚 𝐴)) |
19 | | elmapi 7879 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝐴) → 𝑓:𝐴⟶𝐵) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑓:𝐴⟶𝐵) |
21 | | simp3 1063 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) → 𝐶 ⊆ 𝐴) |
22 | 21 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝐶 ⊆ 𝐴) |
23 | 20, 22 | fssresd 6071 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 ↾ 𝐶):𝐶⟶𝐵) |
24 | | simp2 1062 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) → 𝐵 ∈ 𝑊) |
25 | | simp1 1061 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) → 𝐴 ∈ 𝑉) |
26 | 25, 21 | ssexd 4805 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) → 𝐶 ∈ V) |
27 | | elmapg 7870 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ V) → ((𝑓 ↾ 𝐶) ∈ (𝐵 ↑𝑚 𝐶) ↔ (𝑓 ↾ 𝐶):𝐶⟶𝐵)) |
28 | 24, 26, 27 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) → ((𝑓 ↾ 𝐶) ∈ (𝐵 ↑𝑚 𝐶) ↔ (𝑓 ↾ 𝐶):𝐶⟶𝐵)) |
29 | 28 | ad2antrr 762 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → ((𝑓 ↾ 𝐶) ∈ (𝐵 ↑𝑚 𝐶) ↔ (𝑓 ↾ 𝐶):𝐶⟶𝐵)) |
30 | 23, 29 | mpbird 247 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 ↾ 𝐶) ∈ (𝐵 ↑𝑚 𝐶)) |
31 | 17, 30 | eqeltrd 2701 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑔 ∈ (𝐵 ↑𝑚 𝐶)) |
32 | | undif 4049 |
. . . . . . . . . . 11
⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∪ (𝐴 ∖ 𝐶)) = 𝐴) |
33 | 32 | biimpi 206 |
. . . . . . . . . 10
⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∪ (𝐴 ∖ 𝐶)) = 𝐴) |
34 | 33 | reseq2d 5396 |
. . . . . . . . 9
⊢ (𝐶 ⊆ 𝐴 → (𝑓 ↾ (𝐶 ∪ (𝐴 ∖ 𝐶))) = (𝑓 ↾ 𝐴)) |
35 | 22, 34 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 ↾ (𝐶 ∪ (𝐴 ∖ 𝐶))) = (𝑓 ↾ 𝐴)) |
36 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
37 | | fnresdm 6000 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝐴 → (𝑓 ↾ 𝐴) = 𝑓) |
38 | 20, 36, 37 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 ↾ 𝐴) = 𝑓) |
39 | 35, 38 | eqtr2d 2657 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑓 = (𝑓 ↾ (𝐶 ∪ (𝐴 ∖ 𝐶)))) |
40 | | resundi 5410 |
. . . . . . 7
⊢ (𝑓 ↾ (𝐶 ∪ (𝐴 ∖ 𝐶))) = ((𝑓 ↾ 𝐶) ∪ (𝑓 ↾ (𝐴 ∖ 𝐶))) |
41 | 39, 40 | syl6eq 2672 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑓 = ((𝑓 ↾ 𝐶) ∪ (𝑓 ↾ (𝐴 ∖ 𝐶)))) |
42 | 17 | eqcomd 2628 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 ↾ 𝐶) = 𝑔) |
43 | | simprlr 803 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) |
44 | 25 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝐴 ∈ 𝑉) |
45 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑍 ∈ 𝐵) |
46 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝐵 ∖ {𝑍}) = (𝐵 ∖ {𝑍}) |
47 | 46 | ffs2 29503 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝐵 ∧ 𝑓:𝐴⟶𝐵) → (𝑓 supp 𝑍) = (◡𝑓 “ (𝐵 ∖ {𝑍}))) |
48 | 44, 45, 20, 47 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 supp 𝑍) = (◡𝑓 “ (𝐵 ∖ {𝑍}))) |
49 | | sseqin2 3817 |
. . . . . . . . . . 11
⊢ (𝐶 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐶) = 𝐶) |
50 | 49 | biimpi 206 |
. . . . . . . . . 10
⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶) |
51 | 22, 50 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝐴 ∩ 𝐶) = 𝐶) |
52 | 43, 48, 51 | 3sstr4d 3648 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 supp 𝑍) ⊆ (𝐴 ∩ 𝐶)) |
53 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝑓 ∈ (𝐵 ↑𝑚 𝐴)) |
54 | 53, 19, 36 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝑓 Fn 𝐴) |
55 | | inundif 4046 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐶) ∪ (𝐴 ∖ 𝐶)) = 𝐴 |
56 | 55 | fneq2i 5986 |
. . . . . . . . . . 11
⊢ (𝑓 Fn ((𝐴 ∩ 𝐶) ∪ (𝐴 ∖ 𝐶)) ↔ 𝑓 Fn 𝐴) |
57 | 54, 56 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝑓 Fn ((𝐴 ∩ 𝐶) ∪ (𝐴 ∖ 𝐶))) |
58 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝑓 ∈ V) |
60 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝑍 ∈ 𝐵) |
61 | | inindif 29353 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐶) ∩ (𝐴 ∖ 𝐶)) = ∅ |
62 | 61 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑍 ∈ 𝐵) → ((𝐴 ∩ 𝐶) ∩ (𝐴 ∖ 𝐶)) = ∅) |
63 | | fnsuppres 7322 |
. . . . . . . . . 10
⊢ ((𝑓 Fn ((𝐴 ∩ 𝐶) ∪ (𝐴 ∖ 𝐶)) ∧ (𝑓 ∈ V ∧ 𝑍 ∈ 𝐵) ∧ ((𝐴 ∩ 𝐶) ∩ (𝐴 ∖ 𝐶)) = ∅) → ((𝑓 supp 𝑍) ⊆ (𝐴 ∩ 𝐶) ↔ (𝑓 ↾ (𝐴 ∖ 𝐶)) = ((𝐴 ∖ 𝐶) × {𝑍}))) |
64 | 57, 59, 60, 62, 63 | syl121anc 1331 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑍 ∈ 𝐵) → ((𝑓 supp 𝑍) ⊆ (𝐴 ∩ 𝐶) ↔ (𝑓 ↾ (𝐴 ∖ 𝐶)) = ((𝐴 ∖ 𝐶) × {𝑍}))) |
65 | 18, 45, 64 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → ((𝑓 supp 𝑍) ⊆ (𝐴 ∩ 𝐶) ↔ (𝑓 ↾ (𝐴 ∖ 𝐶)) = ((𝐴 ∖ 𝐶) × {𝑍}))) |
66 | 52, 65 | mpbid 222 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑓 ↾ (𝐴 ∖ 𝐶)) = ((𝐴 ∖ 𝐶) × {𝑍})) |
67 | 42, 66 | uneq12d 3768 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → ((𝑓 ↾ 𝐶) ∪ (𝑓 ↾ (𝐴 ∖ 𝐶))) = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))) |
68 | 41, 67 | eqtrd 2656 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))) |
69 | 31, 68 | jca 554 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) → (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) |
70 | 24 | ad2antrr 762 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝐵 ∈ 𝑊) |
71 | 25 | ad2antrr 762 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝐴 ∈ 𝑉) |
72 | | elmapi 7879 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) → 𝑔:𝐶⟶𝐵) |
73 | 72 | ad2antrl 764 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝑔:𝐶⟶𝐵) |
74 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝑍 ∈ 𝐵) |
75 | | fconst6g 6094 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝐵 → ((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶𝐵) |
76 | 74, 75 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → ((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶𝐵) |
77 | | disjdif 4040 |
. . . . . . . . 9
⊢ (𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅ |
78 | 77 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅) |
79 | | fun2 6067 |
. . . . . . . 8
⊢ (((𝑔:𝐶⟶𝐵 ∧ ((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶𝐵) ∧ (𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅) → (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})):(𝐶 ∪ (𝐴 ∖ 𝐶))⟶𝐵) |
80 | 73, 76, 78, 79 | syl21anc 1325 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})):(𝐶 ∪ (𝐴 ∖ 𝐶))⟶𝐵) |
81 | | simprr 796 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))) |
82 | 81 | eqcomd 2628 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})) = 𝑓) |
83 | 21 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝐶 ⊆ 𝐴) |
84 | 83, 33 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝐶 ∪ (𝐴 ∖ 𝐶)) = 𝐴) |
85 | 82, 84 | feq12d 6033 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → ((𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})):(𝐶 ∪ (𝐴 ∖ 𝐶))⟶𝐵 ↔ 𝑓:𝐴⟶𝐵)) |
86 | 80, 85 | mpbid 222 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝑓:𝐴⟶𝐵) |
87 | | elmapg 7870 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↔ 𝑓:𝐴⟶𝐵)) |
88 | 87 | biimpar 502 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴⟶𝐵) → 𝑓 ∈ (𝐵 ↑𝑚 𝐴)) |
89 | 70, 71, 86, 88 | syl21anc 1325 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝑓 ∈ (𝐵 ↑𝑚 𝐴)) |
90 | 71, 74, 86, 47 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝑓 supp 𝑍) = (◡𝑓 “ (𝐵 ∖ {𝑍}))) |
91 | 81 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))) |
92 | 91 | fveq1d 6193 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (𝑓‘𝑥) = ((𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))‘𝑥)) |
93 | 73 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝑔:𝐶⟶𝐵) |
94 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝑔:𝐶⟶𝐵 → 𝑔 Fn 𝐶) |
95 | 93, 94 | syl 17 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝑔 Fn 𝐶) |
96 | | fconstg 6092 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ 𝐵 → ((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶{𝑍}) |
97 | 96 | ad3antlr 767 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → ((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶{𝑍}) |
98 | | ffn 6045 |
. . . . . . . . . 10
⊢ (((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶{𝑍} → ((𝐴 ∖ 𝐶) × {𝑍}) Fn (𝐴 ∖ 𝐶)) |
99 | 97, 98 | syl 17 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → ((𝐴 ∖ 𝐶) × {𝑍}) Fn (𝐴 ∖ 𝐶)) |
100 | 77 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅) |
101 | | simpr 477 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝑥 ∈ (𝐴 ∖ 𝐶)) |
102 | | fvun2 6270 |
. . . . . . . . 9
⊢ ((𝑔 Fn 𝐶 ∧ ((𝐴 ∖ 𝐶) × {𝑍}) Fn (𝐴 ∖ 𝐶) ∧ ((𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅ ∧ 𝑥 ∈ (𝐴 ∖ 𝐶))) → ((𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))‘𝑥) = (((𝐴 ∖ 𝐶) × {𝑍})‘𝑥)) |
103 | 95, 99, 100, 101, 102 | syl112anc 1330 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → ((𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))‘𝑥) = (((𝐴 ∖ 𝐶) × {𝑍})‘𝑥)) |
104 | | fvconst 6431 |
. . . . . . . . 9
⊢ ((((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶{𝑍} ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (((𝐴 ∖ 𝐶) × {𝑍})‘𝑥) = 𝑍) |
105 | 97, 101, 104 | syl2anc 693 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (((𝐴 ∖ 𝐶) × {𝑍})‘𝑥) = 𝑍) |
106 | 92, 103, 105 | 3eqtrd 2660 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → (𝑓‘𝑥) = 𝑍) |
107 | 86, 106 | suppss 7325 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝑓 supp 𝑍) ⊆ 𝐶) |
108 | 90, 107 | eqsstr3d 3640 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) |
109 | 81 | reseq1d 5395 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝑓 ↾ 𝐶) = ((𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})) ↾ 𝐶)) |
110 | | res0 5400 |
. . . . . . . . . 10
⊢ (((𝐴 ∖ 𝐶) × {𝑍}) ↾ ∅) =
∅ |
111 | | res0 5400 |
. . . . . . . . . 10
⊢ (𝑔 ↾ ∅) =
∅ |
112 | 110, 111 | eqtr4i 2647 |
. . . . . . . . 9
⊢ (((𝐴 ∖ 𝐶) × {𝑍}) ↾ ∅) = (𝑔 ↾ ∅) |
113 | 77 | reseq2i 5393 |
. . . . . . . . 9
⊢ (((𝐴 ∖ 𝐶) × {𝑍}) ↾ (𝐶 ∩ (𝐴 ∖ 𝐶))) = (((𝐴 ∖ 𝐶) × {𝑍}) ↾ ∅) |
114 | 77 | reseq2i 5393 |
. . . . . . . . 9
⊢ (𝑔 ↾ (𝐶 ∩ (𝐴 ∖ 𝐶))) = (𝑔 ↾ ∅) |
115 | 112, 113,
114 | 3eqtr4ri 2655 |
. . . . . . . 8
⊢ (𝑔 ↾ (𝐶 ∩ (𝐴 ∖ 𝐶))) = (((𝐴 ∖ 𝐶) × {𝑍}) ↾ (𝐶 ∩ (𝐴 ∖ 𝐶))) |
116 | 115 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → (𝑔 ↾ (𝐶 ∩ (𝐴 ∖ 𝐶))) = (((𝐴 ∖ 𝐶) × {𝑍}) ↾ (𝐶 ∩ (𝐴 ∖ 𝐶)))) |
117 | | fresaunres1 6077 |
. . . . . . 7
⊢ ((𝑔:𝐶⟶𝐵 ∧ ((𝐴 ∖ 𝐶) × {𝑍}):(𝐴 ∖ 𝐶)⟶𝐵 ∧ (𝑔 ↾ (𝐶 ∩ (𝐴 ∖ 𝐶))) = (((𝐴 ∖ 𝐶) × {𝑍}) ↾ (𝐶 ∩ (𝐴 ∖ 𝐶)))) → ((𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})) ↾ 𝐶) = 𝑔) |
118 | 73, 76, 116, 117 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → ((𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})) ↾ 𝐶) = 𝑔) |
119 | 109, 118 | eqtr2d 2657 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → 𝑔 = (𝑓 ↾ 𝐶)) |
120 | 89, 108, 119 | jca31 557 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) ∧ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍})))) → ((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶))) |
121 | 69, 120 | impbida 877 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → (((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∧ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶) ∧ 𝑔 = (𝑓 ↾ 𝐶)) ↔ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))))) |
122 | 16, 121 | syl5bb 272 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → ((𝑓 ∈ 𝑋 ∧ 𝑔 = (𝑓 ↾ 𝐶)) ↔ (𝑔 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝑓 = (𝑔 ∪ ((𝐴 ∖ 𝐶) × {𝑍}))))) |
123 | 1, 3, 13, 122 | f1od 6885 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝐹:𝑋–1-1-onto→(𝐵 ↑𝑚 𝐶)) |