Step | Hyp | Ref
| Expression |
1 | | fvex 6932 |
. . . 4
⊢ ( L
‘𝐴) ∈
V |
2 | | fvex 6932 |
. . . 4
⊢ ( L
‘𝐵) ∈
V |
3 | 1, 2 | ab2rexex 8016 |
. . 3
⊢ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∈ V |
4 | 3 | a1i 11 |
. 2
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ {𝑥 ∣
∃𝑦 ∈ ( L
‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∈ V) |
5 | | leftssno 27928 |
. . . . . . . . . . 11
⊢ ( L
‘𝐴) ⊆ No |
6 | 5 | sseli 3998 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ( L ‘𝐴) → 𝑦 ∈ No
) |
7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ( L ‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵)) → 𝑦 ∈ No
) |
8 | 7 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → 𝑦 ∈ No
) |
9 | | onsno 28287 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Ons →
𝐵 ∈ No ) |
10 | 9 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ 𝐵 ∈ No ) |
11 | 10 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → 𝐵 ∈ No
) |
12 | 8, 11 | mulscld 28170 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (𝑦 ·s 𝐵) ∈ No
) |
13 | | onsno 28287 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Ons →
𝐴 ∈ No ) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ 𝐴 ∈ No ) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → 𝐴 ∈ No
) |
16 | | leftssno 27928 |
. . . . . . . . . . 11
⊢ ( L
‘𝐵) ⊆ No |
17 | 16 | sseli 3998 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ( L ‘𝐵) → 𝑧 ∈ No
) |
18 | 17 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ( L ‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵)) → 𝑧 ∈ No
) |
19 | 18 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → 𝑧 ∈ No
) |
20 | 15, 19 | mulscld 28170 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (𝐴 ·s 𝑧) ∈ No
) |
21 | 12, 20 | addscld 28022 |
. . . . . 6
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → ((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) ∈ No
) |
22 | 8, 19 | mulscld 28170 |
. . . . . 6
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (𝑦 ·s 𝑧) ∈ No
) |
23 | 21, 22 | subscld 28102 |
. . . . 5
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) ∈ No
) |
24 | | eleq1 2826 |
. . . . 5
⊢ (𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) → (𝑥 ∈ No
↔ (((𝑦
·s 𝐵)
+s (𝐴
·s 𝑧))
-s (𝑦
·s 𝑧))
∈ No )) |
25 | 23, 24 | syl5ibrcom 247 |
. . . 4
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) → 𝑥 ∈ No
)) |
26 | 25 | rexlimdvva 3215 |
. . 3
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (∃𝑦 ∈ ( L
‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) → 𝑥 ∈ No
)) |
27 | 26 | abssdv 4085 |
. 2
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ {𝑥 ∣
∃𝑦 ∈ ( L
‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ⊆ No
) |
28 | 1 | elpw 4626 |
. . . . . 6
⊢ (( L
‘𝐴) ∈ 𝒫
No ↔ ( L ‘𝐴) ⊆ No
) |
29 | 5, 28 | mpbir 231 |
. . . . 5
⊢ ( L
‘𝐴) ∈ 𝒫
No |
30 | | nulssgt 27852 |
. . . . 5
⊢ (( L
‘𝐴) ∈ 𝒫
No → ( L ‘𝐴) <<s ∅) |
31 | 29, 30 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ ( L ‘𝐴)
<<s ∅) |
32 | 2 | elpw 4626 |
. . . . . 6
⊢ (( L
‘𝐵) ∈ 𝒫
No ↔ ( L ‘𝐵) ⊆ No
) |
33 | 16, 32 | mpbir 231 |
. . . . 5
⊢ ( L
‘𝐵) ∈ 𝒫
No |
34 | | nulssgt 27852 |
. . . . 5
⊢ (( L
‘𝐵) ∈ 𝒫
No → ( L ‘𝐵) <<s ∅) |
35 | 33, 34 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ ( L ‘𝐵)
<<s ∅) |
36 | | onscutleft 28294 |
. . . . 5
⊢ (𝐴 ∈ Ons →
𝐴 = (( L ‘𝐴) |s ∅)) |
37 | 36 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ 𝐴 = (( L
‘𝐴) |s
∅)) |
38 | | onscutleft 28294 |
. . . . 5
⊢ (𝐵 ∈ Ons →
𝐵 = (( L ‘𝐵) |s ∅)) |
39 | 38 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ 𝐵 = (( L
‘𝐵) |s
∅)) |
40 | 31, 35, 37, 39 | mulsunif 28185 |
. . 3
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴
·s 𝐵) =
(({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) |s ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}))) |
41 | | rex0 4378 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ∅
∃𝑧 ∈ ∅
𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
42 | 41 | abf 4425 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} = ∅ |
43 | 42 | uneq2i 4182 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ ∅) |
44 | | un0 4413 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ ∅) = {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} |
45 | 43, 44 | eqtri 2762 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} |
46 | | rex0 4378 |
. . . . . . . . 9
⊢ ¬
∃𝑧 ∈ ∅
𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
47 | 46 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ ( L ‘𝐴) → ¬ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))) |
48 | 47 | nrex 3076 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ( L
‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
49 | 48 | abf 4425 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} = ∅ |
50 | | rex0 4378 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ∅
∃𝑧 ∈ ( L
‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
51 | 50 | abf 4425 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} = ∅ |
52 | 49, 51 | uneq12i 4183 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = (∅ ∪
∅) |
53 | | un0 4413 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
54 | 52, 53 | eqtri 2762 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = ∅ |
55 | 45, 54 | oveq12i 7457 |
. . 3
⊢ (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) |s ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))})) = ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} |s ∅) |
56 | 40, 55 | eqtrdi 2790 |
. 2
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴
·s 𝐵) =
({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} |s ∅)) |
57 | 4, 27, 56 | elons2d 28291 |
1
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴
·s 𝐵)
∈ Ons) |