Proof of Theorem suppun
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssun1 4177 | . . . . . 6
⊢ (◡𝐹 “ (V ∖ {𝑍})) ⊆ ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐺 “ (V ∖ {𝑍}))) | 
| 2 |  | cnvun 6161 | . . . . . . . 8
⊢ ◡(𝐹 ∪ 𝐺) = (◡𝐹 ∪ ◡𝐺) | 
| 3 | 2 | imaeq1i 6074 | . . . . . . 7
⊢ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐹 ∪ ◡𝐺) “ (V ∖ {𝑍})) | 
| 4 |  | imaundir 6169 | . . . . . . 7
⊢ ((◡𝐹 ∪ ◡𝐺) “ (V ∖ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐺 “ (V ∖ {𝑍}))) | 
| 5 | 3, 4 | eqtri 2764 | . . . . . 6
⊢ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐺 “ (V ∖ {𝑍}))) | 
| 6 | 1, 5 | sseqtrri 4032 | . . . . 5
⊢ (◡𝐹 “ (V ∖ {𝑍})) ⊆ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) | 
| 7 | 6 | a1i 11 | . . . 4
⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (◡𝐹 “ (V ∖ {𝑍})) ⊆ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍}))) | 
| 8 |  | suppimacnv 8200 | . . . . 5
⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) | 
| 10 |  | suppun.g | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝑉) | 
| 11 |  | unexg 7764 | . . . . . . 7
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ 𝑉) → (𝐹 ∪ 𝐺) ∈ V) | 
| 12 | 11 | adantlr 715 | . . . . . 6
⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝐺 ∈ 𝑉) → (𝐹 ∪ 𝐺) ∈ V) | 
| 13 | 10, 12 | sylan2 593 | . . . . 5
⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝐹 ∪ 𝐺) ∈ V) | 
| 14 |  | simplr 768 | . . . . 5
⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑍 ∈ V) | 
| 15 |  | suppimacnv 8200 | . . . . 5
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) supp 𝑍) = (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍}))) | 
| 16 | 13, 14, 15 | syl2anc 584 | . . . 4
⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝐹 ∪ 𝐺) supp 𝑍) = (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍}))) | 
| 17 | 7, 9, 16 | 3sstr4d 4038 | . . 3
⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) | 
| 18 | 17 | ex 412 | . 2
⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍))) | 
| 19 |  | supp0prc 8189 | . . . 4
⊢ (¬
(𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) | 
| 20 |  | 0ss 4399 | . . . 4
⊢ ∅
⊆ ((𝐹 ∪ 𝐺) supp 𝑍) | 
| 21 | 19, 20 | eqsstrdi 4027 | . . 3
⊢ (¬
(𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) | 
| 22 | 21 | a1d 25 | . 2
⊢ (¬
(𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍))) | 
| 23 | 18, 22 | pm2.61i 182 | 1
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) |