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	$⊢ A \in V$
	brsuccf.2	$⊢ B \in V$
Assertion	brsuccf	$⊢ A 𝖲𝗎𝖼𝖼 B \leftrightarrow B = suc A$

Proof

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

Metamath Proof Explorer

Theorem brsuccf

Proof