Step | Hyp | Ref
| Expression |
1 | | fvex 6935 |
. . . 4
⊢ ( L
‘𝐴) ∈
V |
2 | | fvex 6935 |
. . . 4
⊢ ( L
‘𝐵) ∈
V |
3 | 1, 2 | ab2rexex 8022 |
. . 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 27939 |
. . . . . . . . . . 11
⊢ ( L
‘𝐴) ⊆ No |
6 | 5 | sseli 4004 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ( L ‘𝐴) → 𝑦 ∈ No
) |
7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ( L ‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵)) → 𝑦 ∈ No
) |
8 | 7 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → 𝑦 ∈ No
) |
9 | | onsno 28298 |
. . . . . . . . . 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 28181 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (𝑦 ·s 𝐵) ∈ No
) |
13 | | onsno 28298 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Ons →
𝐴 ∈ No ) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ 𝐴 ∈ No ) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → 𝐴 ∈ No
) |
16 | | leftssno 27939 |
. . . . . . . . . . 11
⊢ ( L
‘𝐵) ⊆ No |
17 | 16 | sseli 4004 |
. . . . . . . . . 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 28181 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (𝐴 ·s 𝑧) ∈ No
) |
21 | 12, 20 | addscld 28033 |
. . . . . 6
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → ((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) ∈ No
) |
22 | 8, 19 | mulscld 28181 |
. . . . . 6
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (𝑦 ·s 𝑧) ∈ No
) |
23 | 21, 22 | subscld 28113 |
. . . . 5
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ (𝑦 ∈ ( L
‘𝐴) ∧ 𝑧 ∈ ( L ‘𝐵))) → (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) ∈ No
) |
24 | | eleq1 2832 |
. . . . 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 3219 |
. . 3
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (∃𝑦 ∈ ( L
‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) → 𝑥 ∈ No
)) |
27 | 26 | abssdv 4091 |
. 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 27863 |
. . . . 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 27863 |
. . . . 5
⊢ (( L
‘𝐵) ∈ 𝒫
No → ( L ‘𝐵) <<s ∅) |
35 | 33, 34 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ ( L ‘𝐵)
<<s ∅) |
36 | | onscutleft 28305 |
. . . . 5
⊢ (𝐴 ∈ Ons →
𝐴 = (( L ‘𝐴) |s ∅)) |
37 | 36 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ 𝐴 = (( L
‘𝐴) |s
∅)) |
38 | | onscutleft 28305 |
. . . . 5
⊢ (𝐵 ∈ Ons →
𝐵 = (( L ‘𝐵) |s ∅)) |
39 | 38 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ 𝐵 = (( L
‘𝐵) |s
∅)) |
40 | 31, 35, 37, 39 | mulsunif 28196 |
. . 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 4383 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ∅
∃𝑧 ∈ ∅
𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
42 | 41 | abf 4429 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} = ∅ |
43 | 42 | uneq2i 4188 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ ∅) |
44 | | un0 4417 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ ∅) = {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} |
45 | 43, 44 | eqtri 2768 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} |
46 | | rex0 4383 |
. . . . . . . . 9
⊢ ¬
∃𝑧 ∈ ∅
𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
47 | 46 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ ( L ‘𝐴) → ¬ ∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))) |
48 | 47 | nrex 3080 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ( L
‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
49 | 48 | abf 4429 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} = ∅ |
50 | | rex0 4383 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ∅
∃𝑧 ∈ ( L
‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧)) |
51 | 50 | abf 4429 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} = ∅ |
52 | 49, 51 | uneq12i 4189 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = (∅ ∪
∅) |
53 | | un0 4417 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
54 | 52, 53 | eqtri 2768 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ∅ 𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ ∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))}) = ∅ |
55 | 45, 54 | oveq12i 7462 |
. . 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 2796 |
. 2
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴
·s 𝐵) =
({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)∃𝑧 ∈ ( L ‘𝐵)𝑥 = (((𝑦 ·s 𝐵) +s (𝐴 ·s 𝑧)) -s (𝑦 ·s 𝑧))} |s ∅)) |
57 | 4, 27, 56 | elons2d 28302 |
1
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴
·s 𝐵)
∈ Ons) |