Proof of Theorem suppssov1
Step | Hyp | Ref
| Expression |
1 | | suppssov1.a |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) |
2 | 1 | elexd 3451 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
3 | 2 | adantll 711 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ V) |
5 | | oveq2 7279 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐵 → (𝑌𝑂𝑣) = (𝑌𝑂𝐵)) |
6 | 5 | eqeq1d 2742 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐵 → ((𝑌𝑂𝑣) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
7 | | suppssov1.o |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) |
8 | 7 | ralrimiva 3110 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
9 | 8 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
10 | 9 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
11 | | suppssov1.b |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
12 | 11 | adantll 711 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
13 | 6, 10, 12 | rspcdva 3563 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → (𝑌𝑂𝐵) = 𝑍) |
14 | | oveq1 7278 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝑌 → (𝐴𝑂𝐵) = (𝑌𝑂𝐵)) |
15 | 14 | eqeq1d 2742 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝑌 → ((𝐴𝑂𝐵) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
16 | 13, 15 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → (𝐴 = 𝑌 → (𝐴𝑂𝐵) = 𝑍)) |
17 | 16 | necon3d 2966 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
18 | | eldifsni 4729 |
. . . . . . . . 9
⊢ ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → (𝐴𝑂𝐵) ≠ 𝑍) |
19 | 17, 18 | impel 506 |
. . . . . . . 8
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ≠ 𝑌) |
20 | | eldifsn 4726 |
. . . . . . . 8
⊢ (𝐴 ∈ (V ∖ {𝑌}) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ 𝑌)) |
21 | 4, 19, 20 | sylanbrc 583 |
. . . . . . 7
⊢
(((((𝐷 ∈ V
∧ 𝑍 ∈ V) ∧
𝜑) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ (V ∖ {𝑌})) |
22 | 21 | ex 413 |
. . . . . 6
⊢ ((((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ∈ (V ∖ {𝑌}))) |
23 | 22 | ss2rabdv 4014 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})} ⊆ {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
24 | | eqid 2740 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) |
25 | | simpll 764 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝐷 ∈ V) |
26 | | simplr 766 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑍 ∈ V) |
27 | 24, 25, 26 | mptsuppdifd 7993 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})}) |
28 | | eqid 2740 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ 𝐴) = (𝑥 ∈ 𝐷 ↦ 𝐴) |
29 | | suppssov1.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑊) |
30 | 29 | adantl 482 |
. . . . . 6
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑌 ∈ 𝑊) |
31 | 28, 25, 30 | mptsuppdifd 7993 |
. . . . 5
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) = {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
32 | 23, 27, 31 | 3sstr4d 3973 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌)) |
33 | | suppssov1.s |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
34 | 33 | adantl 482 |
. . . 4
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) |
35 | 32, 34 | sstrd 3936 |
. . 3
⊢ (((𝐷 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
36 | 35 | ex 413 |
. 2
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)) |
37 | | mptexg 7094 |
. . . . . . 7
⊢ (𝐷 ∈ V → (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
38 | | ovex 7304 |
. . . . . . . . . 10
⊢ (𝐴𝑂𝐵) ∈ V |
39 | 38 | rgenw 3078 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V |
40 | | dmmptg 6144 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐷 (𝐴𝑂𝐵) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = 𝐷 |
42 | | dmexg 7744 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → dom (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
43 | 41, 42 | eqeltrrid 2846 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V → 𝐷 ∈ V) |
44 | 37, 43 | impbii 208 |
. . . . . 6
⊢ (𝐷 ∈ V ↔ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V) |
45 | 44 | anbi1i 624 |
. . . . 5
⊢ ((𝐷 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V)) |
46 | | supp0prc 7971 |
. . . . 5
⊢ (¬
((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
47 | 45, 46 | sylnbi 330 |
. . . 4
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) = ∅) |
48 | | 0ss 4336 |
. . . 4
⊢ ∅
⊆ 𝐿 |
49 | 47, 48 | eqsstrdi 3980 |
. . 3
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |
50 | 49 | a1d 25 |
. 2
⊢ (¬
(𝐷 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)) |
51 | 36, 50 | pm2.61i 182 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) |