Metamath Proof Explorer

Theorem lemsuccf

Description: Lemma for unfolding different forms 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 lemsuccf ( ∃ 𝑥 ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) ↔ 𝐵 = suc 𝐴 )

Proof

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