Step |
Hyp |
Ref |
Expression |
1 |
|
suppssov1.s |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 ) |
2 |
|
suppssov1.o |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑌 𝑂 𝑣 ) = 𝑍 ) |
3 |
|
suppssov1.a |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 ) |
4 |
|
suppssov1.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑅 ) |
5 |
|
suppssov1.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑊 ) |
6 |
3
|
elexd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ V ) |
7 |
6
|
adantll |
⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ V ) |
8 |
7
|
adantr |
⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ∈ V ) |
9 |
|
oveq2 |
⊢ ( 𝑣 = 𝐵 → ( 𝑌 𝑂 𝑣 ) = ( 𝑌 𝑂 𝐵 ) ) |
10 |
9
|
eqeq1d |
⊢ ( 𝑣 = 𝐵 → ( ( 𝑌 𝑂 𝑣 ) = 𝑍 ↔ ( 𝑌 𝑂 𝐵 ) = 𝑍 ) ) |
11 |
2
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 ) |
12 |
11
|
adantl |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ∀ 𝑣 ∈ 𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 ) |
13 |
12
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ∀ 𝑣 ∈ 𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 ) |
14 |
4
|
adantll |
⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑅 ) |
15 |
10 13 14
|
rspcdva |
⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑌 𝑂 𝐵 ) = 𝑍 ) |
16 |
|
oveq1 |
⊢ ( 𝐴 = 𝑌 → ( 𝐴 𝑂 𝐵 ) = ( 𝑌 𝑂 𝐵 ) ) |
17 |
16
|
eqeq1d |
⊢ ( 𝐴 = 𝑌 → ( ( 𝐴 𝑂 𝐵 ) = 𝑍 ↔ ( 𝑌 𝑂 𝐵 ) = 𝑍 ) ) |
18 |
15 17
|
syl5ibrcom |
⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 = 𝑌 → ( 𝐴 𝑂 𝐵 ) = 𝑍 ) ) |
19 |
18
|
necon3d |
⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 𝑂 𝐵 ) ≠ 𝑍 → 𝐴 ≠ 𝑌 ) ) |
20 |
|
eldifsni |
⊢ ( ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) → ( 𝐴 𝑂 𝐵 ) ≠ 𝑍 ) |
21 |
19 20
|
impel |
⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ≠ 𝑌 ) |
22 |
|
eldifsn |
⊢ ( 𝐴 ∈ ( V ∖ { 𝑌 } ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ 𝑌 ) ) |
23 |
8 21 22
|
sylanbrc |
⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) |
24 |
23
|
ex |
⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) ) |
25 |
24
|
ss2rabdv |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) } ⊆ { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } ) |
26 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) |
27 |
|
simpll |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐷 ∈ V ) |
28 |
|
simplr |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑍 ∈ V ) |
29 |
26 27 28
|
mptsuppdifd |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) } ) |
30 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) |
31 |
5
|
adantl |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑌 ∈ 𝑊 ) |
32 |
30 27 31
|
mptsuppdifd |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) = { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } ) |
33 |
25 29 32
|
3sstr4d |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ) |
34 |
1
|
adantl |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 ) |
35 |
33 34
|
sstrd |
⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 ) |
36 |
35
|
ex |
⊢ ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 ) ) |
37 |
|
mptexg |
⊢ ( 𝐷 ∈ V → ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ) |
38 |
|
ovex |
⊢ ( 𝐴 𝑂 𝐵 ) ∈ V |
39 |
38
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝐷 ( 𝐴 𝑂 𝐵 ) ∈ V |
40 |
|
dmmptg |
⊢ ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 𝑂 𝐵 ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = 𝐷 ) |
41 |
39 40
|
ax-mp |
⊢ dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = 𝐷 |
42 |
|
dmexg |
⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ) |
43 |
41 42
|
eqeltrrid |
⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V → 𝐷 ∈ V ) |
44 |
37 43
|
impbii |
⊢ ( 𝐷 ∈ V ↔ ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ) |
45 |
44
|
anbi1i |
⊢ ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ↔ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ∧ 𝑍 ∈ V ) ) |
46 |
|
supp0prc |
⊢ ( ¬ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = ∅ ) |
47 |
45 46
|
sylnbi |
⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = ∅ ) |
48 |
|
0ss |
⊢ ∅ ⊆ 𝐿 |
49 |
47 48
|
eqsstrdi |
⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 ) |
50 |
49
|
a1d |
⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 ) ) |
51 |
36 50
|
pm2.61i |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 ) |