Proof of Theorem suppssov1
Step | Hyp | Ref
| Expression |
1 | | suppssov1.a |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) |
2 | | elex 3185 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
4 | 3 | adantll 746 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ V) |
6 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → (𝐴𝑂𝐵) ≠ 𝑍) |
7 | | suppssov1.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
8 | 7 | adantll 746 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
9 | | suppssov1.o |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) |
10 | 9 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
12 | 11 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
13 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝐵 → (𝑌𝑂𝑣) = (𝑌𝑂𝐵)) |
14 | 13 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐵 → ((𝑌𝑂𝑣) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
15 | 14 | rspcva 3280 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) → (𝑌𝑂𝐵) = 𝑍) |
16 | 8, 12, 15 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → (𝑌𝑂𝐵) = 𝑍) |
17 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 𝑌 → (𝐴𝑂𝐵) = (𝑌𝑂𝐵)) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝑌 → ((𝐴𝑂𝐵) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
19 | 16, 18 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → (𝐴 = 𝑌 → (𝐴𝑂𝐵) = 𝑍)) |
20 | 19 | necon3d 2803 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
21 | 6, 20 | syl5 33 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ≠ 𝑌)) |
22 | 21 | imp 444 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ≠ 𝑌) |
23 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝐴 ∈ (V ∖ {𝑌}) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ 𝑌)) |
24 | 5, 22, 23 | sylanbrc 695 |
. . . . . . 7
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ (V ∖ {𝑌})) |
25 | 24 | ex 449 |
. . . . . 6
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ∈ (V ∖ {𝑌}))) |
26 | 25 | ss2rabdv 3646 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})} ⊆ {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
27 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) |
28 | | simpll 786 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝐷 ∈ V) |
29 | | simplr 788 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑍 ∈ V) |
30 | 27, 28, 29 | mptsuppdifd 7204 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})}) |
31 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ 𝐴) = (𝑥 ∈ 𝐷 ↦ 𝐴) |
32 | | suppssov1.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑊) |
33 | 32 | adantl 481 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑌 ∈ 𝑊) |
34 | 31, 28, 33 | mptsuppdifd 7204 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) = {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
35 | 26, 30, 34 | 3sstr4d 3611 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌)) |
36 | | suppssov1.s |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
37 | 36 | adantl 481 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
38 | 35, 37 | sstrd 3578 |
. . 3
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
39 | 38 | ex 449 |
. 2
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)) |
40 | | mptexg 6389 |
. . . . . . 7
⊢ (𝐷 ∈ V → (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
41 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐴𝑂𝐵) ∈ V |
42 | 41 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V |
43 | | dmmptg 5549 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷 |
45 | | dmexg 6989 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
46 | 44, 45 | syl5eqelr 2693 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → 𝐷 ∈ V) |
47 | 40, 46 | impbii 198 |
. . . . . 6
⊢ (𝐷 ∈ V ↔ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
48 | 47 | anbi1i 727 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V)) |
49 | | supp0prc 7185 |
. . . . 5
⊢ (¬
((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
50 | 48, 49 | sylnbi 319 |
. . . 4
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
51 | | 0ss 3924 |
. . . 4
⊢ ∅
⊆ 𝐿 |
52 | 50, 51 | syl6eqss 3618 |
. . 3
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
53 | 52 | a1d 25 |
. 2
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)) |
54 | 39, 53 | pm2.61i 175 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |