Proof of Theorem ressval3d
Step | Hyp | Ref
| Expression |
1 | | ressval3d.u |
. 2
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
2 | | sspss 3668 |
. . . 4
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) |
3 | | dfpss3 3655 |
. . . . 5
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) |
4 | 3 | orbi1i 541 |
. . . 4
⊢ ((𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵) ↔ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∨ 𝐴 = 𝐵)) |
5 | 2, 4 | bitri 263 |
. . 3
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∨ 𝐴 = 𝐵)) |
6 | | simplr 788 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → ¬ 𝐵 ⊆ 𝐴) |
7 | | ressval3d.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
8 | 7 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 𝑆 ∈ 𝑉) |
9 | | simpl 472 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) → 𝐴 ⊆ 𝐵) |
10 | | ressval3d.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑆) |
11 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑆)
∈ V |
12 | 10, 11 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ V) |
14 | | ssexg 4732 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V) → 𝐴 ∈ V) |
15 | 9, 13, 14 | syl2an 493 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 𝐴 ∈ V) |
16 | | ressval3d.r |
. . . . . . . 8
⊢ 𝑅 = (𝑆 ↾s 𝐴) |
17 | 16, 10 | ressval2 15756 |
. . . . . . 7
⊢ ((¬
𝐵 ⊆ 𝐴 ∧ 𝑆 ∈ 𝑉 ∧ 𝐴 ∈ V) → 𝑅 = (𝑆 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
18 | 6, 8, 15, 17 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 𝑅 = (𝑆 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) |
19 | | ressval3d.e |
. . . . . . . . . 10
⊢ 𝐸 =
(Base‘ndx) |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 𝐸 = (Base‘ndx)) |
21 | | df-ss 3554 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
22 | 21 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴) |
23 | 22 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (𝐴 ∩ 𝐵)) |
24 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐴 ∩ 𝐵)) |
25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 𝐴 = (𝐴 ∩ 𝐵)) |
26 | 20, 25 | opeq12d 4348 |
. . . . . . . 8
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 〈𝐸, 𝐴〉 = 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉) |
27 | 26 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉 = 〈𝐸, 𝐴〉) |
28 | 27 | oveq2d 6565 |
. . . . . 6
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → (𝑆 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉) = (𝑆 sSet 〈𝐸, 𝐴〉)) |
29 | 18, 28 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝜑) → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉)) |
30 | 29 | ex 449 |
. . . 4
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) → (𝜑 → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉))) |
31 | 16 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝑅 = (𝑆 ↾s 𝐴)) |
32 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝑆 ↾s 𝐴) = (𝑆 ↾s 𝐵)) |
33 | 32 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝑆 ↾s 𝐴) = (𝑆 ↾s 𝐵)) |
34 | 7 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝑆 ∈ 𝑉) |
35 | 10 | ressid 15762 |
. . . . . . . 8
⊢ (𝑆 ∈ 𝑉 → (𝑆 ↾s 𝐵) = 𝑆) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝑆 ↾s 𝐵) = 𝑆) |
37 | 31, 33, 36 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝑅 = 𝑆) |
38 | | df-base 15700 |
. . . . . . . 8
⊢ Base =
Slot 1 |
39 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
40 | | ressval3d.f |
. . . . . . . 8
⊢ (𝜑 → Fun 𝑆) |
41 | | ressval3d.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ dom 𝑆) |
42 | 19, 41 | syl5eqelr 2693 |
. . . . . . . 8
⊢ (𝜑 → (Base‘ndx) ∈
dom 𝑆) |
43 | 38, 39, 7, 40, 42 | setsidvald 15721 |
. . . . . . 7
⊢ (𝜑 → 𝑆 = (𝑆 sSet 〈(Base‘ndx),
(Base‘𝑆)〉)) |
44 | 43 | adantl 481 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝑆 = (𝑆 sSet 〈(Base‘ndx),
(Base‘𝑆)〉)) |
45 | 19 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝐸 = (Base‘ndx)) |
46 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝐴 = 𝐵) |
47 | 46, 10 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝐴 = (Base‘𝑆)) |
48 | 45, 47 | opeq12d 4348 |
. . . . . . . 8
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 〈𝐸, 𝐴〉 = 〈(Base‘ndx),
(Base‘𝑆)〉) |
49 | 48 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 〈(Base‘ndx),
(Base‘𝑆)〉 =
〈𝐸, 𝐴〉) |
50 | 49 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝑆 sSet 〈(Base‘ndx),
(Base‘𝑆)〉) =
(𝑆 sSet 〈𝐸, 𝐴〉)) |
51 | 37, 44, 50 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝐴 = 𝐵 ∧ 𝜑) → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉)) |
52 | 51 | ex 449 |
. . . 4
⊢ (𝐴 = 𝐵 → (𝜑 → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉))) |
53 | 30, 52 | jaoi 393 |
. . 3
⊢ (((𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴) ∨ 𝐴 = 𝐵) → (𝜑 → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉))) |
54 | 5, 53 | sylbi 206 |
. 2
⊢ (𝐴 ⊆ 𝐵 → (𝜑 → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉))) |
55 | 1, 54 | mpcom 37 |
1
⊢ (𝜑 → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉)) |