cats1un

Description: Express a word with an extra symbol as the union of the word and the new value. (Contributed by Mario Carneiro, 28-Feb-2016)

		Ref	Expression
	Assertion	cats1un	$⊢ (A \in Word X \land B \in X) \to A ++ ⟨“ B ”⟩ = A \cup \{⟨\|A\|, B⟩\}$

Proof

Step	Hyp	Ref	Expression
1		ccatws1cl	$⊢ (A \in Word X \land B \in X) \to A ++ ⟨“ B ”⟩ \in Word X$
2		wrdf	$⊢ A ++ ⟨“ B ”⟩ \in Word X \to (A ++ ⟨“ B ”⟩) : (0 ..^\|A ++ ⟨“ B ”⟩\|) ⟶ X$
3	1 2	syl	$⊢ (A \in Word X \land B \in X) \to (A ++ ⟨“ B ”⟩) : (0 ..^\|A ++ ⟨“ B ”⟩\|) ⟶ X$
4		ccatws1len	$⊢ A \in Word X \to \|A ++ ⟨“ B ”⟩\| = \|A\| + 1$
5	4	oveq2d	$⊢ A \in Word X \to (0 ..^\|A ++ ⟨“ B ”⟩\|) = (0 ..^\|A\| + 1)$
6		lencl	$⊢ A \in Word X \to \|A\| \in ℕ_{0}$
7		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
8	6 7	eleqtrdi	$⊢ A \in Word X \to \|A\| \in ℤ_{\geq 0}$
9		fzosplitsn	$⊢ \|A\| \in ℤ_{\geq 0} \to (0 ..^\|A\| + 1) = (0 ..^\|A\|) \cup \{\|A\|\}$
10	8 9	syl	$⊢ A \in Word X \to (0 ..^\|A\| + 1) = (0 ..^\|A\|) \cup \{\|A\|\}$
11	5 10	eqtrd	$⊢ A \in Word X \to (0 ..^\|A ++ ⟨“ B ”⟩\|) = (0 ..^\|A\|) \cup \{\|A\|\}$
12	11	adantr	$⊢ (A \in Word X \land B \in X) \to (0 ..^\|A ++ ⟨“ B ”⟩\|) = (0 ..^\|A\|) \cup \{\|A\|\}$
13	12	feq2d	$⊢ (A \in Word X \land B \in X) \to ((A ++ ⟨“ B ”⟩) : (0 ..^\|A ++ ⟨“ B ”⟩\|) ⟶ X \leftrightarrow (A ++ ⟨“ B ”⟩) : (0 ..^\|A\|) \cup \{\|A\|\} ⟶ X)$
14	3 13	mpbid	$⊢ (A \in Word X \land B \in X) \to (A ++ ⟨“ B ”⟩) : (0 ..^\|A\|) \cup \{\|A\|\} ⟶ X$
15	14	ffnd	$⊢ (A \in Word X \land B \in X) \to (A ++ ⟨“ B ”⟩) Fn ((0 ..^\|A\|) \cup \{\|A\|\})$
16		wrdf	$⊢ A \in Word X \to A : (0 ..^\|A\|) ⟶ X$
17	16	adantr	$⊢ (A \in Word X \land B \in X) \to A : (0 ..^\|A\|) ⟶ X$
18		eqid	$⊢ \{⟨\|A\|, B⟩\} = \{⟨\|A\|, B⟩\}$
19		fsng	$⊢ (\|A\| \in ℕ_{0} \land B \in X) \to (\{⟨\|A\|, B⟩\} : \{\|A\|\} ⟶ \{B\} \leftrightarrow \{⟨\|A\|, B⟩\} = \{⟨\|A\|, B⟩\})$
20	18 19	mpbiri	$⊢ (\|A\| \in ℕ_{0} \land B \in X) \to \{⟨\|A\|, B⟩\} : \{\|A\|\} ⟶ \{B\}$
21	6 20	sylan	$⊢ (A \in Word X \land B \in X) \to \{⟨\|A\|, B⟩\} : \{\|A\|\} ⟶ \{B\}$
22		fzodisjsn	$⊢ (0 ..^\|A\|) \cap \{\|A\|\} = \emptyset$
23	22	a1i	$⊢ (A \in Word X \land B \in X) \to (0 ..^\|A\|) \cap \{\|A\|\} = \emptyset$
24		fun	$⊢ ((A : (0 ..^\|A\|) ⟶ X \land \{⟨\|A\|, B⟩\} : \{\|A\|\} ⟶ \{B\}) \land (0 ..^\|A\|) \cap \{\|A\|\} = \emptyset) \to (A \cup \{⟨\|A\|, B⟩\}) : (0 ..^\|A\|) \cup \{\|A\|\} ⟶ X \cup \{B\}$
25	17 21 23 24	syl21anc	$⊢ (A \in Word X \land B \in X) \to (A \cup \{⟨\|A\|, B⟩\}) : (0 ..^\|A\|) \cup \{\|A\|\} ⟶ X \cup \{B\}$
26	25	ffnd	$⊢ (A \in Word X \land B \in X) \to (A \cup \{⟨\|A\|, B⟩\}) Fn ((0 ..^\|A\|) \cup \{\|A\|\})$
27		elun	$⊢ x \in ((0 ..^\|A\|) \cup \{\|A\|\}) \leftrightarrow (x \in (0 ..^\|A\|) \lor x \in \{\|A\|\})$
28		ccats1val1	$⊢ (A \in Word X \land x \in (0 ..^\|A\|)) \to (A ++ ⟨“ B ”⟩) (x) = A (x)$
29	28	adantlr	$⊢ ((A \in Word X \land B \in X) \land x \in (0 ..^\|A\|)) \to (A ++ ⟨“ B ”⟩) (x) = A (x)$
30		simpr	$⊢ ((A \in Word X \land B \in X) \land x \in (0 ..^\|A\|)) \to x \in (0 ..^\|A\|)$
31		fzonel	$⊢ \neg \|A\| \in (0 ..^\|A\|)$
32		nelne2	$⊢ (x \in (0 ..^\|A\|) \land \neg \|A\| \in (0 ..^\|A\|)) \to x \neq \|A\|$
33	30 31 32	sylancl	$⊢ ((A \in Word X \land B \in X) \land x \in (0 ..^\|A\|)) \to x \neq \|A\|$
34	33	necomd	$⊢ ((A \in Word X \land B \in X) \land x \in (0 ..^\|A\|)) \to \|A\| \neq x$
35		fvunsn	$⊢ \|A\| \neq x \to (A \cup \{⟨\|A\|, B⟩\}) (x) = A (x)$
36	34 35	syl	$⊢ ((A \in Word X \land B \in X) \land x \in (0 ..^\|A\|)) \to (A \cup \{⟨\|A\|, B⟩\}) (x) = A (x)$
37	29 36	eqtr4d	$⊢ ((A \in Word X \land B \in X) \land x \in (0 ..^\|A\|)) \to (A ++ ⟨“ B ”⟩) (x) = (A \cup \{⟨\|A\|, B⟩\}) (x)$
38		fvexd	$⊢ (A \in Word X \land B \in X) \to \|A\| \in V$
39		simpr	$⊢ (A \in Word X \land B \in X) \to B \in X$
40	17	fdmd	$⊢ (A \in Word X \land B \in X) \to dom A = (0 ..^\|A\|)$
41	40	eleq2d	$⊢ (A \in Word X \land B \in X) \to (\|A\| \in dom A \leftrightarrow \|A\| \in (0 ..^\|A\|))$
42	31 41	mtbiri	$⊢ (A \in Word X \land B \in X) \to \neg \|A\| \in dom A$
43		fsnunfv	$⊢ (\|A\| \in V \land B \in X \land \neg \|A\| \in dom A) \to (A \cup \{⟨\|A\|, B⟩\}) (\|A\|) = B$
44	38 39 42 43	syl3anc	$⊢ (A \in Word X \land B \in X) \to (A \cup \{⟨\|A\|, B⟩\}) (\|A\|) = B$
45		simpl	$⊢ (A \in Word X \land B \in X) \to A \in Word X$
46		s1cl	$⊢ B \in X \to ⟨“ B ”⟩ \in Word X$
47	46	adantl	$⊢ (A \in Word X \land B \in X) \to ⟨“ B ”⟩ \in Word X$
48		s1len	$⊢ \|⟨“ B ”⟩\| = 1$
49		1nn	$⊢ 1 \in ℕ$
50	48 49	eqeltri	$⊢ \|⟨“ B ”⟩\| \in ℕ$
51		lbfzo0	$⊢ 0 \in (0 ..^\|⟨“ B ”⟩\|) \leftrightarrow \|⟨“ B ”⟩\| \in ℕ$
52	50 51	mpbir	$⊢ 0 \in (0 ..^\|⟨“ B ”⟩\|)$
53	52	a1i	$⊢ (A \in Word X \land B \in X) \to 0 \in (0 ..^\|⟨“ B ”⟩\|)$
54		ccatval3	$⊢ (A \in Word X \land ⟨“ B ”⟩ \in Word X \land 0 \in (0 ..^\|⟨“ B ”⟩\|)) \to (A ++ ⟨“ B ”⟩) (0 + \|A\|) = ⟨“ B ”⟩ (0)$
55	45 47 53 54	syl3anc	$⊢ (A \in Word X \land B \in X) \to (A ++ ⟨“ B ”⟩) (0 + \|A\|) = ⟨“ B ”⟩ (0)$
56		s1fv	$⊢ B \in X \to ⟨“ B ”⟩ (0) = B$
57	56	adantl	$⊢ (A \in Word X \land B \in X) \to ⟨“ B ”⟩ (0) = B$
58	55 57	eqtrd	$⊢ (A \in Word X \land B \in X) \to (A ++ ⟨“ B ”⟩) (0 + \|A\|) = B$
59	6	adantr	$⊢ (A \in Word X \land B \in X) \to \|A\| \in ℕ_{0}$
60	59	nn0cnd	$⊢ (A \in Word X \land B \in X) \to \|A\| \in ℂ$
61	60	addlidd	$⊢ (A \in Word X \land B \in X) \to 0 + \|A\| = \|A\|$
62	61	fveq2d	$⊢ (A \in Word X \land B \in X) \to (A ++ ⟨“ B ”⟩) (0 + \|A\|) = (A ++ ⟨“ B ”⟩) (\|A\|)$
63	44 58 62	3eqtr2rd	$⊢ (A \in Word X \land B \in X) \to (A ++ ⟨“ B ”⟩) (\|A\|) = (A \cup \{⟨\|A\|, B⟩\}) (\|A\|)$
64		elsni	$⊢ x \in \{\|A\|\} \to x = \|A\|$
65	64	fveq2d	$⊢ x \in \{\|A\|\} \to (A ++ ⟨“ B ”⟩) (x) = (A ++ ⟨“ B ”⟩) (\|A\|)$
66	64	fveq2d	$⊢ x \in \{\|A\|\} \to (A \cup \{⟨\|A\|, B⟩\}) (x) = (A \cup \{⟨\|A\|, B⟩\}) (\|A\|)$
67	65 66	eqeq12d	$⊢ x \in \{\|A\|\} \to ((A ++ ⟨“ B ”⟩) (x) = (A \cup \{⟨\|A\|, B⟩\}) (x) \leftrightarrow (A ++ ⟨“ B ”⟩) (\|A\|) = (A \cup \{⟨\|A\|, B⟩\}) (\|A\|))$
68	63 67	syl5ibrcom	$⊢ (A \in Word X \land B \in X) \to (x \in \{\|A\|\} \to (A ++ ⟨“ B ”⟩) (x) = (A \cup \{⟨\|A\|, B⟩\}) (x))$
69	68	imp	$⊢ ((A \in Word X \land B \in X) \land x \in \{\|A\|\}) \to (A ++ ⟨“ B ”⟩) (x) = (A \cup \{⟨\|A\|, B⟩\}) (x)$
70	37 69	jaodan	$⊢ ((A \in Word X \land B \in X) \land (x \in (0 ..^\|A\|) \lor x \in \{\|A\|\})) \to (A ++ ⟨“ B ”⟩) (x) = (A \cup \{⟨\|A\|, B⟩\}) (x)$
71	27 70	sylan2b	$⊢ ((A \in Word X \land B \in X) \land x \in ((0 ..^\|A\|) \cup \{\|A\|\})) \to (A ++ ⟨“ B ”⟩) (x) = (A \cup \{⟨\|A\|, B⟩\}) (x)$
72	15 26 71	eqfnfvd	$⊢ (A \in Word X \land B \in X) \to A ++ ⟨“ B ”⟩ = A \cup \{⟨\|A\|, B⟩\}$

Metamath Proof Explorer

Theorem cats1un

Proof