Step | Hyp | Ref
| Expression |
1 | | funss 5822 |
. . . . . . . . . 10
⊢ (𝐹 ⊆ 𝐺 → (Fun 𝐺 → Fun 𝐹)) |
2 | 1 | impcom 445 |
. . . . . . . . 9
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺) → Fun 𝐹) |
3 | | funfn 5833 |
. . . . . . . . . 10
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
4 | 3 | biimpi 205 |
. . . . . . . . 9
⊢ (Fun
𝐹 → 𝐹 Fn dom 𝐹) |
5 | 2, 4 | syl 17 |
. . . . . . . 8
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺) → 𝐹 Fn dom 𝐹) |
6 | | funfn 5833 |
. . . . . . . . . 10
⊢ (Fun
𝐺 ↔ 𝐺 Fn dom 𝐺) |
7 | 6 | biimpi 205 |
. . . . . . . . 9
⊢ (Fun
𝐺 → 𝐺 Fn dom 𝐺) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺) → 𝐺 Fn dom 𝐺) |
9 | 5, 8 | jca 553 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺) → (𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺)) |
10 | 9 | 3adant3 1074 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺)) |
11 | 10 | adantr 480 |
. . . . 5
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → (𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺)) |
12 | | dmss 5245 |
. . . . . . . 8
⊢ (𝐹 ⊆ 𝐺 → dom 𝐹 ⊆ dom 𝐺) |
13 | 12 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → dom 𝐹 ⊆ dom 𝐺) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → dom 𝐹 ⊆ dom 𝐺) |
15 | | dmexg 6989 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝑉 → dom 𝐺 ∈ V) |
16 | 15 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → dom 𝐺 ∈ V) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → dom 𝐺 ∈ V) |
18 | | simpr 476 |
. . . . . 6
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → 𝑍 ∈ V) |
19 | 14, 17, 18 | 3jca 1235 |
. . . . 5
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → (dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V)) |
20 | 11, 19 | jca 553 |
. . . 4
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → ((𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺) ∧ (dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V))) |
21 | | funssfv 6119 |
. . . . . . . . 9
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝑥 ∈ dom 𝐹) → (𝐺‘𝑥) = (𝐹‘𝑥)) |
22 | 21 | 3expa 1257 |
. . . . . . . 8
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ∈ dom 𝐹) → (𝐺‘𝑥) = (𝐹‘𝑥)) |
23 | | eqeq1 2614 |
. . . . . . . . 9
⊢ ((𝐺‘𝑥) = (𝐹‘𝑥) → ((𝐺‘𝑥) = 𝑍 ↔ (𝐹‘𝑥) = 𝑍)) |
24 | 23 | biimpd 218 |
. . . . . . . 8
⊢ ((𝐺‘𝑥) = (𝐹‘𝑥) → ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) |
25 | 22, 24 | syl 17 |
. . . . . . 7
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ∈ dom 𝐹) → ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) |
26 | 25 | ralrimiva 2949 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺) → ∀𝑥 ∈ dom 𝐹((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) |
27 | 26 | 3adant3 1074 |
. . . . 5
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → ∀𝑥 ∈ dom 𝐹((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) |
28 | 27 | adantr 480 |
. . . 4
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → ∀𝑥 ∈ dom 𝐹((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) |
29 | | suppfnss 7207 |
. . . 4
⊢ (((𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺) ∧ (dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V)) → (∀𝑥 ∈ dom 𝐹((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) |
30 | 20, 28, 29 | sylc 63 |
. . 3
⊢ (((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)) |
31 | 30 | expcom 450 |
. 2
⊢ (𝑍 ∈ V → ((Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) |
32 | | ssid 3587 |
. . . 4
⊢ ∅
⊆ ∅ |
33 | | simpr 476 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → 𝑍 ∈ V) |
34 | 33 | con3i 149 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
(𝐹 ∈ V ∧ 𝑍 ∈ V)) |
35 | | supp0prc 7185 |
. . . . . 6
⊢ (¬
(𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ (¬
𝑍 ∈ V → (𝐹 supp 𝑍) = ∅) |
37 | | simpr 476 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝑍 ∈ V) → 𝑍 ∈ V) |
38 | 37 | con3i 149 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
(𝐺 ∈ V ∧ 𝑍 ∈ V)) |
39 | | supp0prc 7185 |
. . . . . 6
⊢ (¬
(𝐺 ∈ V ∧ 𝑍 ∈ V) → (𝐺 supp 𝑍) = ∅) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ (¬
𝑍 ∈ V → (𝐺 supp 𝑍) = ∅) |
41 | 36, 40 | sseq12d 3597 |
. . . 4
⊢ (¬
𝑍 ∈ V → ((𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍) ↔ ∅ ⊆
∅)) |
42 | 32, 41 | mpbiri 247 |
. . 3
⊢ (¬
𝑍 ∈ V → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)) |
43 | 42 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) |
44 | 31, 43 | pm2.61i 175 |
1
⊢ ((Fun
𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)) |