Step | Hyp | Ref
| Expression |
1 | | suppssov1.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) |
2 | 1 | elexd 3490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
3 | 2 | adantlr 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
4 | 3 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ V) |
5 | | oveq2 7422 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐵 → (𝑌𝑂𝑣) = (𝑌𝑂𝐵)) |
6 | 5 | eqeq1d 2729 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐵 → ((𝑌𝑂𝑣) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
7 | | suppssov1.o |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) |
8 | 7 | ralrimiva 3141 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
9 | 8 | ad2antrr 725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
10 | | suppssov1.b |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
11 | 10 | adantlr 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
12 | 6, 9, 11 | rspcdva 3608 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) → (𝑌𝑂𝐵) = 𝑍) |
13 | | oveq1 7421 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝑌 → (𝐴𝑂𝐵) = (𝑌𝑂𝐵)) |
14 | 13 | eqeq1d 2729 |
. . . . . . . . . 10
⊢ (𝐴 = 𝑌 → ((𝐴𝑂𝐵) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
15 | 12, 14 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) → (𝐴 = 𝑌 → (𝐴𝑂𝐵) = 𝑍)) |
16 | 15 | necon3d 2956 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
17 | | eldifsni 4789 |
. . . . . . . 8
⊢ ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → (𝐴𝑂𝐵) ≠ 𝑍) |
18 | 16, 17 | impel 505 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ≠ 𝑌) |
19 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝐴 ∈ (V ∖ {𝑌}) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ 𝑌)) |
20 | 4, 18, 19 | sylanbrc 582 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ (V ∖ {𝑌})) |
21 | 20 | ex 412 |
. . . . 5
⊢ (((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ∈ (V ∖ {𝑌}))) |
22 | 21 | ss2rabdv 4069 |
. . . 4
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})} ⊆ {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
23 | | eqid 2727 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) |
24 | | simprl 770 |
. . . . 5
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → 𝐷 ∈ V) |
25 | | simprr 772 |
. . . . 5
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → 𝑍 ∈ V) |
26 | 23, 24, 25 | mptsuppdifd 8184 |
. . . 4
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})}) |
27 | | eqid 2727 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 ↦ 𝐴) = (𝑥 ∈ 𝐷 ↦ 𝐴) |
28 | | suppssov1.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑊) |
29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → 𝑌 ∈ 𝑊) |
30 | 27, 24, 29 | mptsuppdifd 8184 |
. . . 4
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) = {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
31 | 22, 26, 30 | 3sstr4d 4025 |
. . 3
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌)) |
32 | | suppssov1.s |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
33 | 32 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
34 | 31, 33 | sstrd 3988 |
. 2
⊢ ((𝜑 ∧ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
35 | | mptexg 7227 |
. . . . . . 7
⊢ (𝐷 ∈ V → (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
36 | | ovex 7447 |
. . . . . . . . . 10
⊢ (𝐴𝑂𝐵) ∈ V |
37 | 36 | rgenw 3060 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V |
38 | | dmmptg 6240 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷 |
40 | | dmexg 7903 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
41 | 39, 40 | eqeltrrid 2833 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → 𝐷 ∈ V) |
42 | 35, 41 | impbii 208 |
. . . . . 6
⊢ (𝐷 ∈ V ↔ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
43 | 42 | anbi1i 623 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V)) |
44 | | supp0prc 8162 |
. . . . 5
⊢ (¬
((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
45 | 43, 44 | sylnbi 330 |
. . . 4
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
46 | | 0ss 4392 |
. . . 4
⊢ ∅
⊆ 𝐿 |
47 | 45, 46 | eqsstrdi 4032 |
. . 3
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
48 | 47 | adantl 481 |
. 2
⊢ ((𝜑 ∧ ¬ (𝐷 ∈ V ∧ 𝑍 ∈ V)) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
49 | 34, 48 | pm2.61dan 812 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |