| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-succf 35874 | . . 3
⊢ Succ =
(Cup ∘ ( I ⊗ Singleton)) | 
| 2 | 1 | breqi 5148 | . 2
⊢ (𝐴Succ𝐵 ↔ 𝐴(Cup ∘ ( I ⊗ Singleton))𝐵) | 
| 3 |  | brsuccf.1 | . . 3
⊢ 𝐴 ∈ V | 
| 4 |  | brsuccf.2 | . . 3
⊢ 𝐵 ∈ V | 
| 5 | 3, 4 | brco 5880 | . 2
⊢ (𝐴(Cup ∘ ( I ⊗
Singleton))𝐵 ↔
∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵)) | 
| 6 |  | opex 5468 | . . . . 5
⊢
〈𝐴, {𝐴}〉 ∈
V | 
| 7 |  | breq1 5145 | . . . . 5
⊢ (𝑥 = 〈𝐴, {𝐴}〉 → (𝑥Cup𝐵 ↔ 〈𝐴, {𝐴}〉Cup𝐵)) | 
| 8 | 6, 7 | ceqsexv 3531 | . . . 4
⊢
(∃𝑥(𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵) ↔ 〈𝐴, {𝐴}〉Cup𝐵) | 
| 9 |  | snex 5435 | . . . . 5
⊢ {𝐴} ∈ V | 
| 10 | 3, 9, 4 | brcup 35941 | . . . 4
⊢
(〈𝐴, {𝐴}〉Cup𝐵 ↔ 𝐵 = (𝐴 ∪ {𝐴})) | 
| 11 | 8, 10 | bitri 275 | . . 3
⊢
(∃𝑥(𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵) ↔ 𝐵 = (𝐴 ∪ {𝐴})) | 
| 12 | 3 | brtxp2 35883 | . . . . . 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 646 | . . . . . . . 8
⊢ (((𝑥 = 〈𝑎, 𝑏〉 ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏)) ∧ 𝑥Cup𝐵) ↔ ((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵) ∧ (𝐴 I 𝑎 ∧ 𝐴Singleton𝑏))) | 
| 17 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑎 ∈ V | 
| 18 | 17 | ideq 5862 | . . . . . . . . . . . 12
⊢ (𝐴 I 𝑎 ↔ 𝐴 = 𝑎) | 
| 19 |  | eqcom 2743 | . . . . . . . . . . . 12
⊢ (𝐴 = 𝑎 ↔ 𝑎 = 𝐴) | 
| 20 | 18, 19 | bitri 275 | . . . . . . . . . . 11
⊢ (𝐴 I 𝑎 ↔ 𝑎 = 𝐴) | 
| 21 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑏 ∈ V | 
| 22 | 3, 21 | brsingle 35919 | . . . . . . . . . . 11
⊢ (𝐴Singleton𝑏 ↔ 𝑏 = {𝐴}) | 
| 23 | 20, 22 | anbi12i 628 | . . . . . . . . . 10
⊢ ((𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐴})) | 
| 24 | 23 | anbi1i 624 | . . . . . . . . 9
⊢ (((𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵)) ↔ ((𝑎 = 𝐴 ∧ 𝑏 = {𝐴}) ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) | 
| 25 |  | ancom 460 | . . . . . . . . 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 1848 | . . . . . 6
⊢
(∃𝑎∃𝑏((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐴} ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵))) | 
| 30 |  | 19.41vv 1949 | . . . . . 6
⊢
(∃𝑎∃𝑏((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵)) | 
| 31 |  | opeq1 4872 | . . . . . . . . 9
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) | 
| 32 | 31 | eqeq2d 2747 | . . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑥 = 〈𝑎, 𝑏〉 ↔ 𝑥 = 〈𝐴, 𝑏〉)) | 
| 33 | 32 | anbi1d 631 | . . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, 𝑏〉 ∧ 𝑥Cup𝐵))) | 
| 34 |  | opeq2 4873 | . . . . . . . . 9
⊢ (𝑏 = {𝐴} → 〈𝐴, 𝑏〉 = 〈𝐴, {𝐴}〉) | 
| 35 | 34 | eqeq2d 2747 | . . . . . . . 8
⊢ (𝑏 = {𝐴} → (𝑥 = 〈𝐴, 𝑏〉 ↔ 𝑥 = 〈𝐴, {𝐴}〉)) | 
| 36 | 35 | anbi1d 631 | . . . . . . 7
⊢ (𝑏 = {𝐴} → ((𝑥 = 〈𝐴, 𝑏〉 ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵))) | 
| 37 | 3, 9, 33, 36 | ceqsex2v 3535 | . . . . . 6
⊢
(∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐴} ∧ (𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑥Cup𝐵)) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) | 
| 38 | 29, 30, 37 | 3bitr3i 301 | . . . . 5
⊢
((∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐴Singleton𝑏) ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) | 
| 39 | 13, 38 | bitri 275 | . . . 4
⊢ ((𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ (𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) | 
| 40 | 39 | exbii 1847 | . . 3
⊢
(∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ ∃𝑥(𝑥 = 〈𝐴, {𝐴}〉 ∧ 𝑥Cup𝐵)) | 
| 41 |  | df-suc 6389 | . . . 4
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | 
| 42 | 41 | eqeq2i 2749 | . . 3
⊢ (𝐵 = suc 𝐴 ↔ 𝐵 = (𝐴 ∪ {𝐴})) | 
| 43 | 11, 40, 42 | 3bitr4i 303 | . 2
⊢
(∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ 𝐵 = suc 𝐴) | 
| 44 | 2, 5, 43 | 3bitri 297 | 1
⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴) |