Step | Hyp | Ref
| Expression |
1 | | oawordeulem.3 |
. . . . . 6
⊢ 𝑆 = {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} |
2 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ On |
3 | 1, 2 | eqsstri 3598 |
. . . . 5
⊢ 𝑆 ⊆ On |
4 | | oawordeulem.2 |
. . . . . . 7
⊢ 𝐵 ∈ On |
5 | | oawordeulem.1 |
. . . . . . . 8
⊢ 𝐴 ∈ On |
6 | | oaword2 7520 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → 𝐵 ⊆ (𝐴 +𝑜 𝐵)) |
7 | 4, 5, 6 | mp2an 704 |
. . . . . . 7
⊢ 𝐵 ⊆ (𝐴 +𝑜 𝐵) |
8 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 𝐵)) |
9 | 8 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 𝐵))) |
10 | 9, 1 | elrab2 3333 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑆 ↔ (𝐵 ∈ On ∧ 𝐵 ⊆ (𝐴 +𝑜 𝐵))) |
11 | 4, 7, 10 | mpbir2an 957 |
. . . . . 6
⊢ 𝐵 ∈ 𝑆 |
12 | 11 | ne0ii 3882 |
. . . . 5
⊢ 𝑆 ≠ ∅ |
13 | | oninton 6892 |
. . . . 5
⊢ ((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ On) |
14 | 3, 12, 13 | mp2an 704 |
. . . 4
⊢ ∩ 𝑆
∈ On |
15 | | onzsl 6938 |
. . . . . . . 8
⊢ (∩ 𝑆
∈ On ↔ (∩ 𝑆 = ∅ ∨ ∃𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))) |
16 | 14, 15 | mpbi 219 |
. . . . . . 7
⊢ (∩ 𝑆 =
∅ ∨ ∃𝑧
∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆)) |
17 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (∩ 𝑆 =
∅ → (𝐴
+𝑜 ∩ 𝑆) = (𝐴 +𝑜
∅)) |
18 | | oa0 7483 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (𝐴 +𝑜 ∅)
= 𝐴) |
19 | 5, 18 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐴 +𝑜 ∅)
= 𝐴 |
20 | 17, 19 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (∩ 𝑆 =
∅ → (𝐴
+𝑜 ∩ 𝑆) = 𝐴) |
21 | 20 | sseq1d 3595 |
. . . . . . . . 9
⊢ (∩ 𝑆 =
∅ → ((𝐴
+𝑜 ∩ 𝑆) ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
22 | 21 | biimprd 237 |
. . . . . . . 8
⊢ (∩ 𝑆 =
∅ → (𝐴 ⊆
𝐵 → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵)) |
23 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (∩ 𝑆 =
suc 𝑧 → (𝐴 +𝑜 ∩ 𝑆) =
(𝐴 +𝑜
suc 𝑧)) |
24 | | oasuc 7491 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ On) → (𝐴 +𝑜 suc 𝑧) = suc (𝐴 +𝑜 𝑧)) |
25 | 5, 24 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ On → (𝐴 +𝑜 suc 𝑧) = suc (𝐴 +𝑜 𝑧)) |
26 | 23, 25 | sylan9eqr 2666 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ ∩ 𝑆 =
suc 𝑧) → (𝐴 +𝑜 ∩ 𝑆) =
suc (𝐴
+𝑜 𝑧)) |
27 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
28 | 27 | sucid 5721 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ suc 𝑧 |
29 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢ (∩ 𝑆 =
suc 𝑧 → (𝑧 ∈ ∩ 𝑆
↔ 𝑧 ∈ suc 𝑧)) |
30 | 28, 29 | mpbiri 247 |
. . . . . . . . . . . . 13
⊢ (∩ 𝑆 =
suc 𝑧 → 𝑧 ∈ ∩ 𝑆) |
31 | 14 | oneli 5752 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ∩ 𝑆
→ 𝑧 ∈
On) |
32 | 1 | inteqi 4414 |
. . . . . . . . . . . . . . . . 17
⊢ ∩ 𝑆 =
∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} |
33 | 32 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ∩ 𝑆
↔ 𝑧 ∈ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) |
34 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 𝑧)) |
35 | 34 | sseq2d 3596 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 𝑧))) |
36 | 35 | onnminsb 6896 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ On → (𝑧 ∈ ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} → ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑧))) |
37 | 33, 36 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ On → (𝑧 ∈ ∩ 𝑆
→ ¬ 𝐵 ⊆
(𝐴 +𝑜
𝑧))) |
38 | | oacl 7502 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ On) → (𝐴 +𝑜 𝑧) ∈ On) |
39 | 5, 38 | mpan 702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ On → (𝐴 +𝑜 𝑧) ∈ On) |
40 | | ontri1 5674 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ On ∧ (𝐴 +𝑜 𝑧) ∈ On) → (𝐵 ⊆ (𝐴 +𝑜 𝑧) ↔ ¬ (𝐴 +𝑜 𝑧) ∈ 𝐵)) |
41 | 4, 39, 40 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ On → (𝐵 ⊆ (𝐴 +𝑜 𝑧) ↔ ¬ (𝐴 +𝑜 𝑧) ∈ 𝐵)) |
42 | 41 | con2bid 343 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ On → ((𝐴 +𝑜 𝑧) ∈ 𝐵 ↔ ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑧))) |
43 | 37, 42 | sylibrd 248 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ On → (𝑧 ∈ ∩ 𝑆
→ (𝐴
+𝑜 𝑧)
∈ 𝐵)) |
44 | 31, 43 | mpcom 37 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∩ 𝑆
→ (𝐴
+𝑜 𝑧)
∈ 𝐵) |
45 | 4 | onordi 5749 |
. . . . . . . . . . . . . 14
⊢ Ord 𝐵 |
46 | | ordsucss 6910 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝐵 → ((𝐴 +𝑜 𝑧) ∈ 𝐵 → suc (𝐴 +𝑜 𝑧) ⊆ 𝐵)) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +𝑜 𝑧) ∈ 𝐵 → suc (𝐴 +𝑜 𝑧) ⊆ 𝐵) |
48 | 30, 44, 47 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (∩ 𝑆 =
suc 𝑧 → suc (𝐴 +𝑜 𝑧) ⊆ 𝐵) |
49 | 48 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ ∩ 𝑆 =
suc 𝑧) → suc (𝐴 +𝑜 𝑧) ⊆ 𝐵) |
50 | 26, 49 | eqsstrd 3602 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ On ∧ ∩ 𝑆 =
suc 𝑧) → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵) |
51 | 50 | rexlimiva 3010 |
. . . . . . . . 9
⊢
(∃𝑧 ∈ On
∩ 𝑆 = suc 𝑧 → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵) |
52 | 51 | a1d 25 |
. . . . . . . 8
⊢
(∃𝑧 ∈ On
∩ 𝑆 = suc 𝑧 → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵)) |
53 | | oalim 7499 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → (𝐴 +𝑜 ∩ 𝑆) =
∪ 𝑧 ∈ ∩ 𝑆(𝐴 +𝑜 𝑧)) |
54 | 5, 53 | mpan 702 |
. . . . . . . . . 10
⊢ ((∩ 𝑆
∈ V ∧ Lim ∩ 𝑆) → (𝐴 +𝑜 ∩ 𝑆) =
∪ 𝑧 ∈ ∩ 𝑆(𝐴 +𝑜 𝑧)) |
55 | | iunss 4497 |
. . . . . . . . . . 11
⊢ (∪ 𝑧 ∈ ∩ 𝑆(𝐴 +𝑜 𝑧) ⊆ 𝐵 ↔ ∀𝑧 ∈ ∩ 𝑆(𝐴 +𝑜 𝑧) ⊆ 𝐵) |
56 | 4 | onelssi 5753 |
. . . . . . . . . . . 12
⊢ ((𝐴 +𝑜 𝑧) ∈ 𝐵 → (𝐴 +𝑜 𝑧) ⊆ 𝐵) |
57 | 44, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ∩ 𝑆
→ (𝐴
+𝑜 𝑧)
⊆ 𝐵) |
58 | 55, 57 | mprgbir 2911 |
. . . . . . . . . 10
⊢ ∪ 𝑧 ∈ ∩ 𝑆(𝐴 +𝑜 𝑧) ⊆ 𝐵 |
59 | 54, 58 | syl6eqss 3618 |
. . . . . . . . 9
⊢ ((∩ 𝑆
∈ V ∧ Lim ∩ 𝑆) → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵) |
60 | 59 | a1d 25 |
. . . . . . . 8
⊢ ((∩ 𝑆
∈ V ∧ Lim ∩ 𝑆) → (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵)) |
61 | 22, 52, 60 | 3jaoi 1383 |
. . . . . . 7
⊢ ((∩ 𝑆 =
∅ ∨ ∃𝑧
∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))
→ (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵)) |
62 | 16, 61 | ax-mp 5 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵) |
63 | 9 | rspcev 3282 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐵 ⊆ (𝐴 +𝑜 𝐵)) → ∃𝑦 ∈ On 𝐵 ⊆ (𝐴 +𝑜 𝑦)) |
64 | 4, 7, 63 | mp2an 704 |
. . . . . . . 8
⊢
∃𝑦 ∈ On
𝐵 ⊆ (𝐴 +𝑜 𝑦) |
65 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐵 |
66 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝐴 |
67 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦
+𝑜 |
68 | | nfrab1 3099 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} |
69 | 68 | nfint 4421 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)} |
70 | 66, 67, 69 | nfov 6575 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) |
71 | 65, 70 | nfss 3561 |
. . . . . . . . 9
⊢
Ⅎ𝑦 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) |
72 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)})) |
73 | 72 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}))) |
74 | 71, 73 | onminsb 6891 |
. . . . . . . 8
⊢
(∃𝑦 ∈ On
𝐵 ⊆ (𝐴 +𝑜 𝑦) → 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)})) |
75 | 64, 74 | ax-mp 5 |
. . . . . . 7
⊢ 𝐵 ⊆ (𝐴 +𝑜 ∩ {𝑦
∈ On ∣ 𝐵 ⊆
(𝐴 +𝑜
𝑦)}) |
76 | 32 | oveq2i 6560 |
. . . . . . 7
⊢ (𝐴 +𝑜 ∩ 𝑆) =
(𝐴 +𝑜
∩ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) |
77 | 75, 76 | sseqtr4i 3601 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 +𝑜 ∩ 𝑆) |
78 | 62, 77 | jctir 559 |
. . . . 5
⊢ (𝐴 ⊆ 𝐵 → ((𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵 ∧ 𝐵 ⊆ (𝐴 +𝑜 ∩ 𝑆))) |
79 | | eqss 3583 |
. . . . 5
⊢ ((𝐴 +𝑜 ∩ 𝑆) =
𝐵 ↔ ((𝐴 +𝑜 ∩ 𝑆)
⊆ 𝐵 ∧ 𝐵 ⊆ (𝐴 +𝑜 ∩ 𝑆))) |
80 | 78, 79 | sylibr 223 |
. . . 4
⊢ (𝐴 ⊆ 𝐵 → (𝐴 +𝑜 ∩ 𝑆) =
𝐵) |
81 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = ∩
𝑆 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 ∩ 𝑆)) |
82 | 81 | eqeq1d 2612 |
. . . . 5
⊢ (𝑥 = ∩
𝑆 → ((𝐴 +𝑜 𝑥) = 𝐵 ↔ (𝐴 +𝑜 ∩ 𝑆) =
𝐵)) |
83 | 82 | rspcev 3282 |
. . . 4
⊢ ((∩ 𝑆
∈ On ∧ (𝐴
+𝑜 ∩ 𝑆) = 𝐵) → ∃𝑥 ∈ On (𝐴 +𝑜 𝑥) = 𝐵) |
84 | 14, 80, 83 | sylancr 694 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → ∃𝑥 ∈ On (𝐴 +𝑜 𝑥) = 𝐵) |
85 | | eqtr3 2631 |
. . . . 5
⊢ (((𝐴 +𝑜 𝑥) = 𝐵 ∧ (𝐴 +𝑜 𝑦) = 𝐵) → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑦)) |
86 | | oacan 7515 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑦) ↔ 𝑥 = 𝑦)) |
87 | 5, 86 | mp3an1 1403 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑦) ↔ 𝑥 = 𝑦)) |
88 | 85, 87 | syl5ib 233 |
. . . 4
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 +𝑜 𝑥) = 𝐵 ∧ (𝐴 +𝑜 𝑦) = 𝐵) → 𝑥 = 𝑦)) |
89 | 88 | rgen2a 2960 |
. . 3
⊢
∀𝑥 ∈ On
∀𝑦 ∈ On
(((𝐴 +𝑜
𝑥) = 𝐵 ∧ (𝐴 +𝑜 𝑦) = 𝐵) → 𝑥 = 𝑦) |
90 | 84, 89 | jctir 559 |
. 2
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ On (𝐴 +𝑜 𝑥) = 𝐵 ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (((𝐴 +𝑜 𝑥) = 𝐵 ∧ (𝐴 +𝑜 𝑦) = 𝐵) → 𝑥 = 𝑦))) |
91 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑦)) |
92 | 91 | eqeq1d 2612 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐴 +𝑜 𝑥) = 𝐵 ↔ (𝐴 +𝑜 𝑦) = 𝐵)) |
93 | 92 | reu4 3367 |
. 2
⊢
(∃!𝑥 ∈ On
(𝐴 +𝑜
𝑥) = 𝐵 ↔ (∃𝑥 ∈ On (𝐴 +𝑜 𝑥) = 𝐵 ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (((𝐴 +𝑜 𝑥) = 𝐵 ∧ (𝐴 +𝑜 𝑦) = 𝐵) → 𝑥 = 𝑦))) |
94 | 90, 93 | sylibr 223 |
1
⊢ (𝐴 ⊆ 𝐵 → ∃!𝑥 ∈ On (𝐴 +𝑜 𝑥) = 𝐵) |