Proof of Theorem suppssov1
Step | Hyp | Ref
| Expression |
1 | | suppssov1.a |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) |
2 | | elex 2610 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
3 | 1, 2 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ V) |
4 | 3 | adantr 270 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ V) |
5 | | eldifsni 3518 |
. . . . . . . 8
⊢ ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → (𝐴𝑂𝐵) ≠ 𝑍) |
6 | | suppssov1.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) |
7 | | suppssov1.o |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) |
8 | 7 | ralrimiva 2434 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
9 | 8 | adantr 270 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) |
10 | | oveq2 5540 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐵 → (𝑌𝑂𝑣) = (𝑌𝑂𝐵)) |
11 | 10 | eqeq1d 2089 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐵 → ((𝑌𝑂𝑣) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
12 | 11 | rspcva 2699 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑣 ∈ 𝑅 (𝑌𝑂𝑣) = 𝑍) → (𝑌𝑂𝐵) = 𝑍) |
13 | 6, 9, 12 | syl2anc 403 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑌𝑂𝐵) = 𝑍) |
14 | | oveq1 5539 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝑌 → (𝐴𝑂𝐵) = (𝑌𝑂𝐵)) |
15 | 14 | eqeq1d 2089 |
. . . . . . . . . 10
⊢ (𝐴 = 𝑌 → ((𝐴𝑂𝐵) = 𝑍 ↔ (𝑌𝑂𝐵) = 𝑍)) |
16 | 13, 15 | syl5ibrcom 155 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐴 = 𝑌 → (𝐴𝑂𝐵) = 𝑍)) |
17 | 16 | necon3d 2289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ≠ 𝑍 → 𝐴 ≠ 𝑌)) |
18 | 5, 17 | syl5 32 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ≠ 𝑌)) |
19 | 18 | imp 122 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ≠ 𝑌) |
20 | | eldifsn 3517 |
. . . . . 6
⊢ (𝐴 ∈ (V ∖ {𝑌}) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ 𝑌)) |
21 | 4, 19, 20 | sylanbrc 408 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})) → 𝐴 ∈ (V ∖ {𝑌})) |
22 | 21 | ex 113 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐴𝑂𝐵) ∈ (V ∖ {𝑍}) → 𝐴 ∈ (V ∖ {𝑌}))) |
23 | 22 | ss2rabdv 3075 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})} ⊆ {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})}) |
24 | | eqid 2081 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) = (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) |
25 | 24 | mptpreima 4834 |
. . 3
⊢ (◡(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) “ (V ∖ {𝑍})) = {𝑥 ∈ 𝐷 ∣ (𝐴𝑂𝐵) ∈ (V ∖ {𝑍})} |
26 | | eqid 2081 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ 𝐴) = (𝑥 ∈ 𝐷 ↦ 𝐴) |
27 | 26 | mptpreima 4834 |
. . 3
⊢ (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌})) = {𝑥 ∈ 𝐷 ∣ 𝐴 ∈ (V ∖ {𝑌})} |
28 | 23, 25, 27 | 3sstr4g 3040 |
. 2
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) “ (V ∖ {𝑍})) ⊆ (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌}))) |
29 | | suppssov1.s |
. 2
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿) |
30 | 28, 29 | sstrd 3009 |
1
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) “ (V ∖ {𝑍})) ⊆ 𝐿) |