| Step | Hyp | Ref
| Expression |
| 1 | | suppovss.1 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) |
| 2 | 1 | ralrimivva 3202 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷) |
| 3 | | suppovss.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| 4 | 3 | fmpo 8093 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
| 5 | 2, 4 | sylib 218 |
. 2
⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)⟶𝐷) |
| 6 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑧 = 〈𝑥, 𝑦〉) |
| 7 | 6 | fveq2d 6910 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑧) = (𝐹‘〈𝑥, 𝑦〉)) |
| 8 | | df-ov 7434 |
. . . . . . . 8
⊢ (𝑥𝐹𝑦) = (𝐹‘〈𝑥, 𝑦〉) |
| 9 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) |
| 10 | 9 | eldifad 3963 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑥 ∈ 𝐴) |
| 11 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑦 ∈ 𝐵) |
| 12 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝜑) |
| 13 | 12, 10, 11, 1 | syl12anc 837 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐶 ∈ 𝐷) |
| 14 | 3 | ovmpt4g 7580 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) → (𝑥𝐹𝑦) = 𝐶) |
| 15 | 10, 11, 13, 14 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝑥𝐹𝑦) = 𝐶) |
| 16 | 8, 15 | eqtr3id 2791 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘〈𝑥, 𝑦〉) = 𝐶) |
| 17 | | suppovss.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 19 | 18 | mptexd 7244 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V) |
| 20 | | suppovss.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ 𝐶)) |
| 21 | 19, 20 | fmptd 7134 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:𝐴⟶V) |
| 22 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 supp (𝐵 × {𝑍})) ⊆ (𝐺 supp (𝐵 × {𝑍}))) |
| 23 | | suppovss.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 24 | | snex 5436 |
. . . . . . . . . . . . 13
⊢ {𝑍} ∈ V |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑍} ∈ V) |
| 26 | 17, 25 | xpexd 7771 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 × {𝑍}) ∈ V) |
| 27 | 21, 22, 23, 26 | suppssr 8220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) → (𝐺‘𝑥) = (𝐵 × {𝑍})) |
| 28 | 27 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) → ((𝐺‘𝑥)‘𝑦) = ((𝐵 × {𝑍})‘𝑦)) |
| 29 | 12, 9, 28 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑥)‘𝑦) = ((𝐵 × {𝑍})‘𝑦)) |
| 30 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 31 | 20 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V) → (𝐺‘𝑥) = (𝑦 ∈ 𝐵 ↦ 𝐶)) |
| 32 | 30, 19, 31 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝑦 ∈ 𝐵 ↦ 𝐶)) |
| 33 | 1 | anassrs 467 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐷) |
| 34 | 32, 33 | fvmpt2d 7029 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑥)‘𝑦) = 𝐶) |
| 35 | 12, 10, 11, 34 | syl21anc 838 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑥)‘𝑦) = 𝐶) |
| 36 | | suppovss.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ 𝐷) |
| 37 | 12, 36 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑍 ∈ 𝐷) |
| 38 | | fvconst2g 7222 |
. . . . . . . . 9
⊢ ((𝑍 ∈ 𝐷 ∧ 𝑦 ∈ 𝐵) → ((𝐵 × {𝑍})‘𝑦) = 𝑍) |
| 39 | 37, 11, 38 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → ((𝐵 × {𝑍})‘𝑦) = 𝑍) |
| 40 | 29, 35, 39 | 3eqtr3d 2785 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐶 = 𝑍) |
| 41 | 7, 16, 40 | 3eqtrd 2781 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑧) = 𝑍) |
| 42 | 41 | adantl3r 750 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵)) ∧ 𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑧) = 𝑍) |
| 43 | | elxp2 5709 |
. . . . . . 7
⊢ (𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵) ↔ ∃𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))∃𝑦 ∈ 𝐵 𝑧 = 〈𝑥, 𝑦〉) |
| 44 | 43 | biimpi 216 |
. . . . . 6
⊢ (𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵) → ∃𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))∃𝑦 ∈ 𝐵 𝑧 = 〈𝑥, 𝑦〉) |
| 45 | 44 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵)) → ∃𝑥 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))∃𝑦 ∈ 𝐵 𝑧 = 〈𝑥, 𝑦〉) |
| 46 | 42, 45 | r19.29vva 3216 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵)) → (𝐹‘𝑧) = 𝑍) |
| 47 | 46 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) ∧ 𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵)) → (𝐹‘𝑧) = 𝑍) |
| 48 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑧 = 〈𝑥, 𝑦〉) |
| 49 | 48 | fveq2d 6910 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑧) = (𝐹‘〈𝑥, 𝑦〉)) |
| 50 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑥 ∈ 𝐴) |
| 51 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) |
| 52 | 51 | eldifad 3963 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝑦 ∈ 𝐵) |
| 53 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝜑) |
| 54 | 53, 50, 52, 1 | syl12anc 837 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐶 ∈ 𝐷) |
| 55 | 50, 52, 54, 14 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝑥𝐹𝑦) = 𝐶) |
| 56 | 8, 55 | eqtr3id 2791 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘〈𝑥, 𝑦〉) = 𝐶) |
| 57 | 53, 50, 52, 34 | syl21anc 838 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑥)‘𝑦) = 𝐶) |
| 58 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑥)‘𝑦) ∈ V) |
| 59 | 33, 32, 58 | fmpt2d 7144 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥):𝐵⟶V) |
| 60 | | ssiun2 5047 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((𝐺‘𝑥) supp 𝑍) ⊆ ∪ 𝑥 ∈ 𝐴 ((𝐺‘𝑥) supp 𝑍)) |
| 61 | 60 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) supp 𝑍) ⊆ ∪ 𝑥 ∈ 𝐴 ((𝐺‘𝑥) supp 𝑍)) |
| 62 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → (𝐺‘𝑥) = (𝐺‘𝑘)) |
| 63 | 62 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) supp 𝑍) = ((𝐺‘𝑘) supp 𝑍)) |
| 64 | 63 | cbviunv 5040 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ 𝐴 ((𝐺‘𝑥) supp 𝑍) = ∪
𝑘 ∈ 𝐴 ((𝐺‘𝑘) supp 𝑍) |
| 65 | 61, 64 | sseqtrdi 4024 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) supp 𝑍) ⊆ ∪ 𝑘 ∈ 𝐴 ((𝐺‘𝑘) supp 𝑍)) |
| 66 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) → 𝜑) |
| 67 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) → 𝑘 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) |
| 68 | 67 | eldifad 3963 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) → 𝑘 ∈ 𝐴) |
| 69 | 21, 22, 23, 26 | suppssr 8220 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) → (𝐺‘𝑘) = (𝐵 × {𝑍})) |
| 70 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑘 → (𝑥 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴)) |
| 71 | 70 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑘 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑘 ∈ 𝐴))) |
| 72 | 62 | fneq1d 6661 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) Fn 𝐵 ↔ (𝐺‘𝑘) Fn 𝐵)) |
| 73 | 71, 72 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑘 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) Fn 𝐵) ↔ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) Fn 𝐵))) |
| 74 | 59 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) Fn 𝐵) |
| 75 | 73, 74 | chvarvv 1998 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) Fn 𝐵) |
| 76 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 77 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑍 ∈ 𝐷) |
| 78 | | fnsuppeq0 8217 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺‘𝑘) Fn 𝐵 ∧ 𝐵 ∈ 𝑊 ∧ 𝑍 ∈ 𝐷) → (((𝐺‘𝑘) supp 𝑍) = ∅ ↔ (𝐺‘𝑘) = (𝐵 × {𝑍}))) |
| 79 | 75, 76, 77, 78 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (((𝐺‘𝑘) supp 𝑍) = ∅ ↔ (𝐺‘𝑘) = (𝐵 × {𝑍}))) |
| 80 | 79 | biimpar 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ (𝐺‘𝑘) = (𝐵 × {𝑍})) → ((𝐺‘𝑘) supp 𝑍) = ∅) |
| 81 | 66, 68, 69, 80 | syl21anc 838 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) → ((𝐺‘𝑘) supp 𝑍) = ∅) |
| 82 | 81 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))((𝐺‘𝑘) supp 𝑍) = ∅) |
| 83 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) |
| 84 | 83 | iunxdif3 5095 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))((𝐺‘𝑘) supp 𝑍) = ∅ → ∪ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))))((𝐺‘𝑘) supp 𝑍) = ∪
𝑘 ∈ 𝐴 ((𝐺‘𝑘) supp 𝑍)) |
| 85 | 82, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))))((𝐺‘𝑘) supp 𝑍) = ∪
𝑘 ∈ 𝐴 ((𝐺‘𝑘) supp 𝑍)) |
| 86 | | dfin4 4278 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∩ (𝐺 supp (𝐵 × {𝑍}))) = (𝐴 ∖ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) |
| 87 | | suppssdm 8202 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 supp (𝐵 × {𝑍})) ⊆ dom 𝐺 |
| 88 | 87, 21 | fssdm 6755 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺 supp (𝐵 × {𝑍})) ⊆ 𝐴) |
| 89 | | sseqin2 4223 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 supp (𝐵 × {𝑍})) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐺 supp (𝐵 × {𝑍}))) = (𝐺 supp (𝐵 × {𝑍}))) |
| 90 | 88, 89 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∩ (𝐺 supp (𝐵 × {𝑍}))) = (𝐺 supp (𝐵 × {𝑍}))) |
| 91 | 86, 90 | eqtr3id 2791 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 ∖ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍})))) = (𝐺 supp (𝐵 × {𝑍}))) |
| 92 | 91 | iuneq1d 5019 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))))((𝐺‘𝑘) supp 𝑍) = ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)) |
| 93 | 85, 92 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 ((𝐺‘𝑘) supp 𝑍) = ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
𝑘 ∈ 𝐴 ((𝐺‘𝑘) supp 𝑍) = ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)) |
| 95 | 65, 94 | sseqtrd 4020 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) supp 𝑍) ⊆ ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)) |
| 96 | 36 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑍 ∈ 𝐷) |
| 97 | 59, 95, 18, 96 | suppssr 8220 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) → ((𝐺‘𝑥)‘𝑦) = 𝑍) |
| 98 | 97 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → ((𝐺‘𝑥)‘𝑦) = 𝑍) |
| 99 | 57, 98 | eqtr3d 2779 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → 𝐶 = 𝑍) |
| 100 | 49, 56, 99 | 3eqtrd 2781 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑧) = 𝑍) |
| 101 | 100 | adantl3r 750 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ∧ 𝑧 = 〈𝑥, 𝑦〉) → (𝐹‘𝑧) = 𝑍) |
| 102 | | elxp2 5709 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))𝑧 = 〈𝑥, 𝑦〉) |
| 103 | 102 | biimpi 216 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))𝑧 = 〈𝑥, 𝑦〉) |
| 104 | 103 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))𝑧 = 〈𝑥, 𝑦〉) |
| 105 | 101, 104 | r19.29vva 3216 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) → (𝐹‘𝑧) = 𝑍) |
| 106 | 105 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) ∧ 𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) → (𝐹‘𝑧) = 𝑍) |
| 107 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) → 𝑧 ∈ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) |
| 108 | | difxp 6184 |
. . . . 5
⊢ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) = (((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵) ∪ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) |
| 109 | 107, 108 | eleqtrdi 2851 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) → 𝑧 ∈ (((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵) ∪ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))))) |
| 110 | | elun 4153 |
. . . 4
⊢ (𝑧 ∈ (((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵) ∪ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) ↔ (𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵) ∨ 𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))))) |
| 111 | 109, 110 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) → (𝑧 ∈ ((𝐴 ∖ (𝐺 supp (𝐵 × {𝑍}))) × 𝐵) ∨ 𝑧 ∈ (𝐴 × (𝐵 ∖ ∪
𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))))) |
| 112 | 47, 106, 111 | mpjaodan 961 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴 × 𝐵) ∖ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))) → (𝐹‘𝑧) = 𝑍) |
| 113 | 5, 112 | suppss 8219 |
1
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) |