Step | Hyp | Ref
| Expression |
1 | | fvex 6932 |
. . . . 5
⊢ ( L
‘𝐴) ∈
V |
2 | 1 | abrexex 7999 |
. . . 4
⊢ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∈ V |
3 | | fvex 6932 |
. . . . 5
⊢ ( L
‘𝐵) ∈
V |
4 | 3 | abrexex 7999 |
. . . 4
⊢ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)} ∈ V |
5 | 2, 4 | unex 7775 |
. . 3
⊢ ({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)}) ∈ V |
6 | 5 | a1i 11 |
. 2
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ ({𝑥 ∣
∃𝑦 ∈ ( L
‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)}) ∈ V) |
7 | | leftssno 27928 |
. . . . . . . . 9
⊢ ( L
‘𝐴) ⊆ No |
8 | 7 | sseli 3998 |
. . . . . . . 8
⊢ (𝑦 ∈ ( L ‘𝐴) → 𝑦 ∈ No
) |
9 | 8 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐴)) → 𝑦 ∈
No ) |
10 | | onsno 28287 |
. . . . . . . 8
⊢ (𝐵 ∈ Ons →
𝐵 ∈ No ) |
11 | 10 | ad2antlr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐴)) → 𝐵 ∈
No ) |
12 | 9, 11 | addscld 28022 |
. . . . . 6
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐴)) → (𝑦 +s 𝐵) ∈ No
) |
13 | | eleq1 2826 |
. . . . . 6
⊢ (𝑥 = (𝑦 +s 𝐵) → (𝑥 ∈ No
↔ (𝑦 +s
𝐵) ∈ No )) |
14 | 12, 13 | syl5ibrcom 247 |
. . . . 5
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐴)) → (𝑥 = (𝑦 +s 𝐵) → 𝑥 ∈ No
)) |
15 | 14 | rexlimdva 3157 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (∃𝑦 ∈ ( L
‘𝐴)𝑥 = (𝑦 +s 𝐵) → 𝑥 ∈ No
)) |
16 | 15 | abssdv 4085 |
. . 3
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ {𝑥 ∣
∃𝑦 ∈ ( L
‘𝐴)𝑥 = (𝑦 +s 𝐵)} ⊆ No
) |
17 | | onsno 28287 |
. . . . . . . 8
⊢ (𝐴 ∈ Ons →
𝐴 ∈ No ) |
18 | 17 | ad2antrr 725 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐵)) → 𝐴 ∈
No ) |
19 | | leftssno 27928 |
. . . . . . . . 9
⊢ ( L
‘𝐵) ⊆ No |
20 | 19 | sseli 3998 |
. . . . . . . 8
⊢ (𝑦 ∈ ( L ‘𝐵) → 𝑦 ∈ No
) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐵)) → 𝑦 ∈
No ) |
22 | 18, 21 | addscld 28022 |
. . . . . 6
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐵)) → (𝐴 +s 𝑦) ∈
No ) |
23 | | eleq1 2826 |
. . . . . 6
⊢ (𝑥 = (𝐴 +s 𝑦) → (𝑥 ∈ No
↔ (𝐴 +s
𝑦) ∈ No )) |
24 | 22, 23 | syl5ibrcom 247 |
. . . . 5
⊢ (((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
∧ 𝑦 ∈ ( L
‘𝐵)) → (𝑥 = (𝐴 +s 𝑦) → 𝑥 ∈ No
)) |
25 | 24 | rexlimdva 3157 |
. . . 4
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (∃𝑦 ∈ ( L
‘𝐵)𝑥 = (𝐴 +s 𝑦) → 𝑥 ∈ No
)) |
26 | 25 | abssdv 4085 |
. . 3
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ {𝑥 ∣
∃𝑦 ∈ ( L
‘𝐵)𝑥 = (𝐴 +s 𝑦)} ⊆ No
) |
27 | 16, 26 | unssd 4209 |
. 2
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ ({𝑥 ∣
∃𝑦 ∈ ( L
‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)}) ⊆ No
) |
28 | 1 | elpw 4626 |
. . . . . 6
⊢ (( L
‘𝐴) ∈ 𝒫
No ↔ ( L ‘𝐴) ⊆ No
) |
29 | 7, 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 | 3 | elpw 4626 |
. . . . . 6
⊢ (( L
‘𝐵) ∈ 𝒫
No ↔ ( L ‘𝐵) ⊆ No
) |
33 | 19, 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 | addsunif 28044 |
. . 3
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴 +s
𝐵) = (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝐴 +s 𝑦)}))) |
41 | | rex0 4378 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ∅
𝑥 = (𝑦 +s 𝐵) |
42 | 41 | abf 4425 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 𝐵)} = ∅ |
43 | | rex0 4378 |
. . . . . . 7
⊢ ¬
∃𝑦 ∈ ∅
𝑥 = (𝐴 +s 𝑦) |
44 | 43 | abf 4425 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝐴 +s 𝑦)} = ∅ |
45 | 42, 44 | uneq12i 4183 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝐴 +s 𝑦)}) = (∅ ∪
∅) |
46 | | un0 4413 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
47 | 45, 46 | eqtri 2762 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝐴 +s 𝑦)}) = ∅ |
48 | 47 | oveq2i 7456 |
. . 3
⊢ (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝐴 +s 𝑦)})) = (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)}) |s ∅) |
49 | 40, 48 | eqtrdi 2790 |
. 2
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴 +s
𝐵) = (({𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐴)𝑥 = (𝑦 +s 𝐵)} ∪ {𝑥 ∣ ∃𝑦 ∈ ( L ‘𝐵)𝑥 = (𝐴 +s 𝑦)}) |s ∅)) |
50 | 6, 27, 49 | elons2d 28291 |
1
⊢ ((𝐴 ∈ Ons ∧
𝐵 ∈ Ons)
→ (𝐴 +s
𝐵) ∈
Ons) |