Proof of Theorem suppss3
Step | Hyp | Ref
| Expression |
1 | | suppss3.1 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
2 | 1 | oveq1i 7223 |
. 2
⊢ (𝐺 supp 𝑍) = ((𝑥 ∈ 𝐴 ↦ 𝐵) supp 𝑍) |
3 | | simpl 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐹 supp 𝑍))) → 𝜑) |
4 | | eldifi 4041 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ (𝐹 supp 𝑍)) → 𝑥 ∈ 𝐴) |
5 | 4 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐹 supp 𝑍))) → 𝑥 ∈ 𝐴) |
6 | | suppss3.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 Fn 𝐴) |
7 | | suppss3.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
8 | | fnex 7033 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
9 | 6, 7, 8 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
10 | | suppss3.z |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
11 | | suppimacnv 7916 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
12 | 9, 10, 11 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
13 | 12 | eleq2d 2823 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝐹 supp 𝑍) ↔ 𝑥 ∈ (◡𝐹 “ (V ∖ {𝑍})))) |
14 | | elpreima 6878 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ (◡𝐹 “ (V ∖ {𝑍})) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ {𝑍})))) |
15 | 6, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (◡𝐹 “ (V ∖ {𝑍})) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ {𝑍})))) |
16 | 13, 15 | bitrd 282 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝐹 supp 𝑍) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (V ∖ {𝑍})))) |
17 | 16 | baibd 543 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐹 supp 𝑍) ↔ (𝐹‘𝑥) ∈ (V ∖ {𝑍}))) |
18 | 17 | notbid 321 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ (𝐹 supp 𝑍) ↔ ¬ (𝐹‘𝑥) ∈ (V ∖ {𝑍}))) |
19 | 18 | biimpd 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ (𝐹 supp 𝑍) → ¬ (𝐹‘𝑥) ∈ (V ∖ {𝑍}))) |
20 | 19 | expimpd 457 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐹 supp 𝑍)) → ¬ (𝐹‘𝑥) ∈ (V ∖ {𝑍}))) |
21 | | eldif 3876 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ (𝐹 supp 𝑍)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐹 supp 𝑍))) |
22 | | fvex 6730 |
. . . . . . . 8
⊢ (𝐹‘𝑥) ∈ V |
23 | | eldifsn 4700 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (V ∖ {𝑍}) ↔ ((𝐹‘𝑥) ∈ V ∧ (𝐹‘𝑥) ≠ 𝑍)) |
24 | 22, 23 | mpbiran 709 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ (V ∖ {𝑍}) ↔ (𝐹‘𝑥) ≠ 𝑍) |
25 | 24 | necon2bbii 2992 |
. . . . . 6
⊢ ((𝐹‘𝑥) = 𝑍 ↔ ¬ (𝐹‘𝑥) ∈ (V ∖ {𝑍})) |
26 | 20, 21, 25 | 3imtr4g 299 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ (𝐹 supp 𝑍)) → (𝐹‘𝑥) = 𝑍)) |
27 | 26 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐹 supp 𝑍))) → (𝐹‘𝑥) = 𝑍) |
28 | | suppss3.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑍) → 𝐵 = 𝑍) |
29 | 3, 5, 27, 28 | syl3anc 1373 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐹 supp 𝑍))) → 𝐵 = 𝑍) |
30 | 29, 7 | suppss2 7942 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ (𝐹 supp 𝑍)) |
31 | 2, 30 | eqsstrid 3949 |
1
⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑍)) |