Metamath Proof Explorer

Theorem brsuccf

Description: Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brsuccf.1 ⊢ 𝐴 ∈ V
brsuccf.2 ⊢ 𝐵 ∈ V
Assertion brsuccf ( 𝐴 Succ 𝐵 ↔ 𝐵 = suc 𝐴 )

Proof

Step Hyp Ref Expression
1 brsuccf.1 ⊢ 𝐴 ∈ V
2 brsuccf.2 ⊢ 𝐵 ∈ V
3 df-succf ⊢ Succ = ( Cup ∘ ( I ⊗ Singleton ) )
4 3 breqi ⊢ ( 𝐴 Succ 𝐵 ↔ 𝐴 ( Cup ∘ ( I ⊗ Singleton ) ) 𝐵 )
5 1 2 brco ⊢ ( 𝐴 ( Cup ∘ ( I ⊗ Singleton ) ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) )
6 opex ⊢ ⟨ 𝐴 , { 𝐴 } ⟩ ∈ V
7 breq1 ⊢ ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ → ( 𝑥 Cup 𝐵 ↔ ⟨ 𝐴 , { 𝐴 } ⟩ Cup 𝐵 ) )
8 6 7 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ∧ 𝑥 Cup 𝐵 ) ↔ ⟨ 𝐴 , { 𝐴 } ⟩ Cup 𝐵 )
9 snex ⊢ { 𝐴 } ∈ V
10 1 9 2 brcup ⊢ ( ⟨ 𝐴 , { 𝐴 } ⟩ Cup 𝐵 ↔ 𝐵 = ( 𝐴 ∪ { 𝐴 } ) )
11 8 10 bitri ⊢ ( ∃ 𝑥 ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ∧ 𝑥 Cup 𝐵 ) ↔ 𝐵 = ( 𝐴 ∪ { 𝐴 } ) )
12 1 brtxp2 ⊢ ( 𝐴 ( I ⊗ Singleton ) 𝑥 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) )
13 12 anbi1i ⊢ ( ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ 𝑥 Cup 𝐵 ) )
14 3anass ⊢ ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ↔ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ) )
15 14 anbi1i ⊢ ( ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ 𝑥 Cup 𝐵 ) ↔ ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ) ∧ 𝑥 Cup 𝐵 ) )
16 an32 ⊢ ( ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ) ∧ 𝑥 Cup 𝐵 ) ↔ ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ∧ ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ) )
17 vex ⊢ 𝑎 ∈ V
18 17 ideq ⊢ ( 𝐴 I 𝑎 ↔ 𝐴 = 𝑎 )
19 eqcom ⊢ ( 𝐴 = 𝑎 ↔ 𝑎 = 𝐴 )
20 18 19 bitri ⊢ ( 𝐴 I 𝑎 ↔ 𝑎 = 𝐴 )
21 vex ⊢ 𝑏 ∈ V
22 1 21 brsingle ⊢ ( 𝐴 Singleton 𝑏 ↔ 𝑏 = { 𝐴 } )
23 20 22 anbi12i ⊢ ( ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ) )
24 23 anbi1i ⊢ ( ( ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) ↔ ( ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ) ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
25 ancom ⊢ ( ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ∧ ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ) ↔ ( ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
26 df-3an ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) ↔ ( ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ) ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
27 24 25 26 3bitr4i ⊢ ( ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ∧ ( 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ) ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
28 15 16 27 3bitri ⊢ ( ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ 𝑥 Cup 𝐵 ) ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
29 28 2exbii ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ 𝑥 Cup 𝐵 ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
30 19.41vv ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ 𝑥 Cup 𝐵 ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ 𝑥 Cup 𝐵 ) )
31 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
32 31 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑥 = ⟨ 𝐴 , 𝑏 ⟩ ) )
33 32 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ↔ ( 𝑥 = ⟨ 𝐴 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
34 opeq2 ⊢ ( 𝑏 = { 𝐴 } → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , { 𝐴 } ⟩ )
35 34 eqeq2d ⊢ ( 𝑏 = { 𝐴 } → ( 𝑥 = ⟨ 𝐴 , 𝑏 ⟩ ↔ 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ) )
36 35 anbi1d ⊢ ( 𝑏 = { 𝐴 } → ( ( 𝑥 = ⟨ 𝐴 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ↔ ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ∧ 𝑥 Cup 𝐵 ) ) )
37 1 9 33 36 ceqsex2v ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐴 } ∧ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑥 Cup 𝐵 ) ) ↔ ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ∧ 𝑥 Cup 𝐵 ) )
38 29 30 37 3bitr3i ⊢ ( ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐴 Singleton 𝑏 ) ∧ 𝑥 Cup 𝐵 ) ↔ ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ∧ 𝑥 Cup 𝐵 ) )
39 13 38 bitri ⊢ ( ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) ↔ ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ∧ 𝑥 Cup 𝐵 ) )
40 39 exbii ⊢ ( ∃ 𝑥 ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 = ⟨ 𝐴 , { 𝐴 } ⟩ ∧ 𝑥 Cup 𝐵 ) )
41 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
42 41 eqeq2i ⊢ ( 𝐵 = suc 𝐴 ↔ 𝐵 = ( 𝐴 ∪ { 𝐴 } ) )
43 11 40 42 3bitr4i ⊢ ( ∃ 𝑥 ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) ↔ 𝐵 = suc 𝐴 )
44 4 5 43 3bitri ⊢ ( 𝐴 Succ 𝐵 ↔ 𝐵 = suc 𝐴 )