Proof of Theorem suppssov1
Step | Hyp | Ref
| Expression |
1 | | suppssov1.a |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) |
2 | | elex 3430 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
4 | 3 | adantll 707 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
5 | 4 | adantr 474 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ V) |
6 | | eldifsni 4541 |
. . . . . . . . . 10
⊢ ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → (𝐴𝑂𝐵) ≠ 𝑍) |
7 | | oveq2 6914 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐵 → (𝑌𝑂𝑣) = (𝑌𝑂𝐵)) |
8 | 7 | eqeq1d 2828 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐵 → ((𝑌𝑂𝑣) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
9 | | suppssov1.o |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) |
10 | 9 | ralrimiva 3176 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
11 | 10 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
12 | 11 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
13 | | suppssov1.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
14 | 13 | adantll 707 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
15 | 8, 12, 14 | rspcdva 3533 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → (𝑌𝑂𝐵) = 𝑍) |
16 | | oveq1 6913 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 𝑌 → (𝐴𝑂𝐵) = (𝑌𝑂𝐵)) |
17 | 16 | eqeq1d 2828 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝑌 → ((𝐴𝑂𝐵) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
18 | 15, 17 | syl5ibrcom 239 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → (𝐴 = 𝑌 → (𝐴𝑂𝐵) = 𝑍)) |
19 | 18 | necon3d 3021 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
20 | 6, 19 | syl5 34 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ≠ 𝑌)) |
21 | 20 | imp 397 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ≠ 𝑌) |
22 | | eldifsn 4537 |
. . . . . . . 8
⊢ (𝐴 ∈ (V ∖ {𝑌}) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ 𝑌)) |
23 | 5, 21, 22 | sylanbrc 580 |
. . . . . . 7
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ (V ∖ {𝑌})) |
24 | 23 | ex 403 |
. . . . . 6
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ∈ (V ∖ {𝑌}))) |
25 | 24 | ss2rabdv 3909 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})} ⊆ {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
26 | | eqid 2826 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) |
27 | | simpll 785 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝐷 ∈ V) |
28 | | simplr 787 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑍 ∈ V) |
29 | 26, 27, 28 | mptsuppdifd 7582 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})}) |
30 | | eqid 2826 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ 𝐴) = (𝑥 ∈ 𝐷 ↦ 𝐴) |
31 | | suppssov1.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑊) |
32 | 31 | adantl 475 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑌 ∈ 𝑊) |
33 | 30, 27, 32 | mptsuppdifd 7582 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) = {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
34 | 25, 29, 33 | 3sstr4d 3874 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌)) |
35 | | suppssov1.s |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
36 | 35 | adantl 475 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
37 | 34, 36 | sstrd 3838 |
. . 3
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
38 | 37 | ex 403 |
. 2
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)) |
39 | | mptexg 6741 |
. . . . . . 7
⊢ (𝐷 ∈ V → (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
40 | | ovex 6938 |
. . . . . . . . . 10
⊢ (𝐴𝑂𝐵) ∈ V |
41 | 40 | rgenw 3134 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V |
42 | | dmmptg 5874 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷 |
44 | | dmexg 7359 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
45 | 43, 44 | syl5eqelr 2912 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → 𝐷 ∈ V) |
46 | 39, 45 | impbii 201 |
. . . . . 6
⊢ (𝐷 ∈ V ↔ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
47 | 46 | anbi1i 619 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V)) |
48 | | supp0prc 7563 |
. . . . 5
⊢ (¬
((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
49 | 47, 48 | sylnbi 322 |
. . . 4
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
50 | | 0ss 4198 |
. . . 4
⊢ ∅
⊆ 𝐿 |
51 | 49, 50 | syl6eqss 3881 |
. . 3
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
52 | 51 | a1d 25 |
. 2
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)) |
53 | 38, 52 | pm2.61i 177 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |