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	$⊢ A \in V$
	brsuccf.2	$⊢ B \in V$
Assertion	lemsuccf	$⊢ \exists x (A (I \otimes 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) x \land x 𝖢𝗎𝗉 B) \leftrightarrow B = suc A$

Proof

Step	Hyp	Ref	Expression
1		brsuccf.1	$⊢ A \in V$
2		brsuccf.2	$⊢ B \in V$
3		opex	$⊢ ⟨A, \{A\}⟩ \in V$
4		breq1	$⊢ x = ⟨A, \{A\}⟩ \to (x 𝖢𝗎𝗉 B \leftrightarrow ⟨A, \{A\}⟩ 𝖢𝗎𝗉 B)$
5	3 4	ceqsexv	$⊢ \exists x (x = ⟨A, \{A\}⟩ \land x 𝖢𝗎𝗉 B) \leftrightarrow ⟨A, \{A\}⟩ 𝖢𝗎𝗉 B$
6		snex	$⊢ \{A\} \in V$
7	1 6 2	brcup	$⊢ ⟨A, \{A\}⟩ 𝖢𝗎𝗉 B \leftrightarrow B = A \cup \{A\}$
8	5 7	bitri	$⊢ \exists x (x = ⟨A, \{A\}⟩ \land x 𝖢𝗎𝗉 B) \leftrightarrow B = A \cup \{A\}$
9	1	brtxp2	$⊢ A (I \otimes 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) x \leftrightarrow \exists a \exists b (x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b)$
10	9	anbi1i	$⊢ (A (I \otimes 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) x \land x 𝖢𝗎𝗉 B) \leftrightarrow (\exists a \exists b (x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land x 𝖢𝗎𝗉 B)$
11		3anass	$⊢ (x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \leftrightarrow (x = ⟨a, b⟩ \land (A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b))$
12	11	anbi1i	$⊢ ((x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land x 𝖢𝗎𝗉 B) \leftrightarrow ((x = ⟨a, b⟩ \land (A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b)) \land x 𝖢𝗎𝗉 B)$
13		an32	$⊢ ((x = ⟨a, b⟩ \land (A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b)) \land x 𝖢𝗎𝗉 B) \leftrightarrow ((x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B) \land (A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b))$
14		vex	$⊢ a \in V$
15	14	ideq	$⊢ A I a \leftrightarrow A = a$
16		eqcom	$⊢ A = a \leftrightarrow a = A$
17	15 16	bitri	$⊢ A I a \leftrightarrow a = A$
18		vex	$⊢ b \in V$
19	1 18	brsingle	$⊢ A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b \leftrightarrow b = \{A\}$
20	17 19	anbi12i	$⊢ (A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \leftrightarrow (a = A \land b = \{A\})$
21	20	anbi1i	$⊢ ((A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B)) \leftrightarrow ((a = A \land b = \{A\}) \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B))$
22		ancom	$⊢ ((x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B) \land (A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b)) \leftrightarrow ((A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B))$
23		df-3an	$⊢ (a = A \land b = \{A\} \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B)) \leftrightarrow ((a = A \land b = \{A\}) \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B))$
24	21 22 23	3bitr4i	$⊢ ((x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B) \land (A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b)) \leftrightarrow (a = A \land b = \{A\} \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B))$
25	12 13 24	3bitri	$⊢ ((x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land x 𝖢𝗎𝗉 B) \leftrightarrow (a = A \land b = \{A\} \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B))$
26	25	2exbii	$⊢ \exists a \exists b ((x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land x 𝖢𝗎𝗉 B) \leftrightarrow \exists a \exists b (a = A \land b = \{A\} \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B))$
27		19.41vv	$⊢ \exists a \exists b ((x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land x 𝖢𝗎𝗉 B) \leftrightarrow (\exists a \exists b (x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land x 𝖢𝗎𝗉 B)$
28		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
29	28	eqeq2d	$⊢ a = A \to (x = ⟨a, b⟩ \leftrightarrow x = ⟨A, b⟩)$
30	29	anbi1d	$⊢ a = A \to ((x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B) \leftrightarrow (x = ⟨A, b⟩ \land x 𝖢𝗎𝗉 B))$
31		opeq2	$⊢ b = \{A\} \to ⟨A, b⟩ = ⟨A, \{A\}⟩$
32	31	eqeq2d	$⊢ b = \{A\} \to (x = ⟨A, b⟩ \leftrightarrow x = ⟨A, \{A\}⟩)$
33	32	anbi1d	$⊢ b = \{A\} \to ((x = ⟨A, b⟩ \land x 𝖢𝗎𝗉 B) \leftrightarrow (x = ⟨A, \{A\}⟩ \land x 𝖢𝗎𝗉 B))$
34	1 6 30 33	ceqsex2v	$⊢ \exists a \exists b (a = A \land b = \{A\} \land (x = ⟨a, b⟩ \land x 𝖢𝗎𝗉 B)) \leftrightarrow (x = ⟨A, \{A\}⟩ \land x 𝖢𝗎𝗉 B)$
35	26 27 34	3bitr3i	$⊢ (\exists a \exists b (x = ⟨a, b⟩ \land A I a \land A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \land x 𝖢𝗎𝗉 B) \leftrightarrow (x = ⟨A, \{A\}⟩ \land x 𝖢𝗎𝗉 B)$
36	10 35	bitri	$⊢ (A (I \otimes 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) x \land x 𝖢𝗎𝗉 B) \leftrightarrow (x = ⟨A, \{A\}⟩ \land x 𝖢𝗎𝗉 B)$
37	36	exbii	$⊢ \exists x (A (I \otimes 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) x \land x 𝖢𝗎𝗉 B) \leftrightarrow \exists x (x = ⟨A, \{A\}⟩ \land x 𝖢𝗎𝗉 B)$
38		df-suc	$⊢ suc A = A \cup \{A\}$
39	38	eqeq2i	$⊢ B = suc A \leftrightarrow B = A \cup \{A\}$
40	8 37 39	3bitr4i	$⊢ \exists x (A (I \otimes 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) x \land x 𝖢𝗎𝗉 B) \leftrightarrow B = suc A$

Metamath Proof Explorer

Theorem lemsuccf

Proof