| Step | Hyp | Ref
| Expression |
| 1 | | simpr1 1195 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → 𝐴 ⊆ 𝐵) |
| 2 | | fndm 6671 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
| 3 | 2 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → dom 𝐹 = 𝐴) |
| 4 | | fndm 6671 |
. . . . . . 7
⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) |
| 5 | 4 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → dom 𝐺 = 𝐵) |
| 6 | 1, 3, 5 | 3sstr4d 4039 |
. . . . 5
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → dom 𝐹 ⊆ dom 𝐺) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) → dom 𝐹 ⊆ dom 𝐺) |
| 8 | 2 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴)) |
| 9 | 8 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴)) |
| 10 | | fveqeq2 6915 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝐺‘𝑥) = 𝑍 ↔ (𝐺‘𝑦) = 𝑍)) |
| 11 | | fveqeq2 6915 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = 𝑍 ↔ (𝐹‘𝑦) = 𝑍)) |
| 12 | 10, 11 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) ↔ ((𝐺‘𝑦) = 𝑍 → (𝐹‘𝑦) = 𝑍))) |
| 13 | 12 | rspcv 3618 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → ((𝐺‘𝑦) = 𝑍 → (𝐹‘𝑦) = 𝑍))) |
| 14 | 9, 13 | biimtrdi 253 |
. . . . . . . . . 10
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (𝑦 ∈ dom 𝐹 → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → ((𝐺‘𝑦) = 𝑍 → (𝐹‘𝑦) = 𝑍)))) |
| 15 | 14 | com23 86 |
. . . . . . . . 9
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝑦 ∈ dom 𝐹 → ((𝐺‘𝑦) = 𝑍 → (𝐹‘𝑦) = 𝑍)))) |
| 16 | 15 | imp31 417 |
. . . . . . . 8
⊢
(((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) ∧ 𝑦 ∈ dom 𝐹) → ((𝐺‘𝑦) = 𝑍 → (𝐹‘𝑦) = 𝑍)) |
| 17 | 16 | necon3d 2961 |
. . . . . . 7
⊢
(((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ≠ 𝑍 → (𝐺‘𝑦) ≠ 𝑍)) |
| 18 | 17 | ex 412 |
. . . . . 6
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) → (𝑦 ∈ dom 𝐹 → ((𝐹‘𝑦) ≠ 𝑍 → (𝐺‘𝑦) ≠ 𝑍))) |
| 19 | 18 | com23 86 |
. . . . 5
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) → ((𝐹‘𝑦) ≠ 𝑍 → (𝑦 ∈ dom 𝐹 → (𝐺‘𝑦) ≠ 𝑍))) |
| 20 | 19 | 3imp 1111 |
. . . 4
⊢
(((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) ∧ (𝐹‘𝑦) ≠ 𝑍 ∧ 𝑦 ∈ dom 𝐹) → (𝐺‘𝑦) ≠ 𝑍) |
| 21 | 7, 20 | rabssrabd 4083 |
. . 3
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) → {𝑦 ∈ dom 𝐹 ∣ (𝐹‘𝑦) ≠ 𝑍} ⊆ {𝑦 ∈ dom 𝐺 ∣ (𝐺‘𝑦) ≠ 𝑍}) |
| 22 | | fnfun 6668 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
| 23 | 22 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → Fun 𝐹) |
| 24 | | simpl 482 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐹 Fn 𝐴) |
| 25 | | ssexg 5323 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) |
| 26 | 25 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝐴 ∈ V) |
| 27 | | fnex 7237 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V) → 𝐹 ∈ V) |
| 28 | 24, 26, 27 | syl2an 596 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → 𝐹 ∈ V) |
| 29 | | simpr3 1197 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → 𝑍 ∈ 𝑊) |
| 30 | | suppval1 8191 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = {𝑦 ∈ dom 𝐹 ∣ (𝐹‘𝑦) ≠ 𝑍}) |
| 31 | 23, 28, 29, 30 | syl3anc 1373 |
. . . . 5
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (𝐹 supp 𝑍) = {𝑦 ∈ dom 𝐹 ∣ (𝐹‘𝑦) ≠ 𝑍}) |
| 32 | | fnfun 6668 |
. . . . . . 7
⊢ (𝐺 Fn 𝐵 → Fun 𝐺) |
| 33 | 32 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → Fun 𝐺) |
| 34 | | simpr 484 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐺 Fn 𝐵) |
| 35 | | simp2 1138 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝐵 ∈ 𝑉) |
| 36 | | fnex 7237 |
. . . . . . 7
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐺 ∈ V) |
| 37 | 34, 35, 36 | syl2an 596 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → 𝐺 ∈ V) |
| 38 | | suppval1 8191 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐺 ∈ V ∧ 𝑍 ∈ 𝑊) → (𝐺 supp 𝑍) = {𝑦 ∈ dom 𝐺 ∣ (𝐺‘𝑦) ≠ 𝑍}) |
| 39 | 33, 37, 29, 38 | syl3anc 1373 |
. . . . 5
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (𝐺 supp 𝑍) = {𝑦 ∈ dom 𝐺 ∣ (𝐺‘𝑦) ≠ 𝑍}) |
| 40 | 31, 39 | sseq12d 4017 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → ((𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍) ↔ {𝑦 ∈ dom 𝐹 ∣ (𝐹‘𝑦) ≠ 𝑍} ⊆ {𝑦 ∈ dom 𝐺 ∣ (𝐺‘𝑦) ≠ 𝑍})) |
| 41 | 40 | adantr 480 |
. . 3
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) → ((𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍) ↔ {𝑦 ∈ dom 𝐹 ∣ (𝐹‘𝑦) ≠ 𝑍} ⊆ {𝑦 ∈ dom 𝐺 ∣ (𝐺‘𝑦) ≠ 𝑍})) |
| 42 | 21, 41 | mpbird 257 |
. 2
⊢ ((((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) ∧ ∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍)) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)) |
| 43 | 42 | ex 412 |
1
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) |