Step | Hyp | Ref
| Expression |
1 | | df-succf 34174 |
. . 3
⊢ Succ =
(Cup ∘ ( I ⊗ Singleton)) |
2 | 1 | breqi 5080 |
. 2
⊢ (𝐴Succ𝐵 ↔ 𝐴(Cup ∘ ( I ⊗ Singleton))𝐵) |
3 | | brsuccf.1 |
. . 3
⊢ 𝐴 ∈ V |
4 | | brsuccf.2 |
. . 3
⊢ 𝐵 ∈ V |
5 | 3, 4 | brco 5779 |
. 2
⊢ (𝐴(Cup ∘ ( I ⊗
Singleton))𝐵 ↔
∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵)) |
6 | | opex 5379 |
. . . . 5
⊢
〈𝐴, {𝐴}〉 ∈
V |
7 | | breq1 5077 |
. . . . 5
⊢ (𝑥 = 〈𝐴, {𝐴}〉 → (𝑥Cup𝐵 ↔ 〈𝐴, {𝐴}〉Cup𝐵)) |
8 | 6, 7 | ceqsexv 3479 |
. . . 4
⊢
(∃𝑥(𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵) ↔ 〈𝐴, {𝐴}〉Cup𝐵) |
9 | | snex 5354 |
. . . . 5
⊢ {𝐴} ∈ V |
10 | 3, 9, 4 | brcup 34241 |
. . . 4
⊢
(〈𝐴, {𝐴}〉Cup𝐵 ↔ 𝐵 = (𝐴 ∪ {𝐴})) |
11 | 8, 10 | bitri 274 |
. . 3
⊢
(∃𝑥(𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵) ↔ 𝐵 = (𝐴 ∪ {𝐴})) |
12 | 3 | brtxp2 34183 |
. . . . . 6
⊢ (𝐴( I ⊗ Singleton)𝑥 ↔ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏)) |
13 | 12 | anbi1i 624 |
. . . . 5
⊢ ((𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵)) |
14 | | 3anass 1094 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ↔ (𝑥 = 〈𝑎, 𝑏〉 ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏))) |
15 | 14 | anbi1i 624 |
. . . . . . . 8
⊢ (((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ ((𝑥 = 〈𝑎, 𝑏〉 ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏)) ∧ 𝑥Cup𝐵)) |
16 | | an32 643 |
. . . . . . . 8
⊢ (((𝑥 = 〈𝑎, 𝑏〉 ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏)) ∧ 𝑥Cup𝐵) ↔ ((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵) ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏))) |
17 | | vex 3436 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
18 | 17 | ideq 5761 |
. . . . . . . . . . . 12
⊢ (𝐴 I 𝑎 ↔ 𝐴 = 𝑎) |
19 | | eqcom 2745 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝑎 ↔ 𝑎 = 𝐴) |
20 | 18, 19 | bitri 274 |
. . . . . . . . . . 11
⊢ (𝐴 I 𝑎 ↔ 𝑎 = 𝐴) |
21 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑏 ∈ V |
22 | 3, 21 | brsingle 34219 |
. . . . . . . . . . 11
⊢ (𝐴Singleton𝑏 ↔ 𝑏 = {𝐴}) |
23 | 20, 22 | anbi12i 627 |
. . . . . . . . . 10
⊢ ((𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐴})) |
24 | 23 | anbi1i 624 |
. . . . . . . . 9
⊢ (((𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵)) ↔ ((𝑎 = 𝐴 ∧ 𝑏 = {𝐴}) ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) |
25 | | ancom 461 |
. . . . . . . . 9
⊢ (((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵) ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏)) ↔ ((𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) |
26 | | df-3an 1088 |
. . . . . . . . 9
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝐴} ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵)) ↔ ((𝑎 = 𝐴 ∧ 𝑏 = {𝐴}) ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) |
27 | 24, 25, 26 | 3bitr4i 303 |
. . . . . . . 8
⊢ (((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵) ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏)) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐴} ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) |
28 | 15, 16, 27 | 3bitri 297 |
. . . . . . 7
⊢ (((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐴} ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) |
29 | 28 | 2exbii 1851 |
. . . . . 6
⊢
(∃𝑎∃𝑏((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐴} ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) |
30 | | 19.41vv 1954 |
. . . . . 6
⊢
(∃𝑎∃𝑏((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵)) |
31 | | opeq1 4804 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
32 | 31 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑥 = 〈𝑎, 𝑏〉 ↔ 𝑥 = 〈𝐴, 𝑏〉)) |
33 | 32 | anbi1d 630 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, 𝑏〉 ∧ 𝑥Cup𝐵))) |
34 | | opeq2 4805 |
. . . . . . . . 9
⊢ (𝑏 = {𝐴} → 〈𝐴, 𝑏〉 = 〈𝐴, {𝐴}〉) |
35 | 34 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑏 = {𝐴} → (𝑥 = 〈𝐴, 𝑏〉 ↔ 𝑥 = 〈𝐴, {𝐴}〉)) |
36 | 35 | anbi1d 630 |
. . . . . . 7
⊢ (𝑏 = {𝐴} → ((𝑥 = 〈𝐴, 𝑏〉 ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵))) |
37 | 3, 9, 33, 36 | ceqsex2v 3483 |
. . . . . 6
⊢
(∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐴} ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵)) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) |
38 | 29, 30, 37 | 3bitr3i 301 |
. . . . 5
⊢
((∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) |
39 | 13, 38 | bitri 274 |
. . . 4
⊢ ((𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) |
40 | 39 | exbii 1850 |
. . 3
⊢
(∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ ∃𝑥(𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) |
41 | | df-suc 6272 |
. . . 4
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
42 | 41 | eqeq2i 2751 |
. . 3
⊢ (𝐵 = suc 𝐴 ↔ 𝐵 = (𝐴 ∪ {𝐴})) |
43 | 11, 40, 42 | 3bitr4i 303 |
. 2
⊢
(∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ 𝐵 = suc 𝐴) |
44 | 2, 5, 43 | 3bitri 297 |
1
⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴) |