ltbval

Description: Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	ltbval.c	$⊢ C = T <_{bag} I$
	ltbval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	ltbval.i	$⊢ φ \to I \in V$
	ltbval.t	$⊢ φ \to T \in W$
Assertion	ltbval	$⊢ φ \to C = \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\}$

Proof

Step	Hyp	Ref	Expression
1		ltbval.c	$⊢ C = T <_{bag} I$
2		ltbval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
3		ltbval.i	$⊢ φ \to I \in V$
4		ltbval.t	$⊢ φ \to T \in W$
5		elex	$⊢ T \in W \to T \in V$
6		elex	$⊢ I \in V \to I \in V$
7		simpr	$⊢ (r = T \land i = I) \to i = I$
8	7	oveq2d	$⊢ (r = T \land i = I) \to {ℕ_{0}}^{i} = {ℕ_{0}}^{I}$
9		rabeq	$⊢ {ℕ_{0}}^{i} = {ℕ_{0}}^{I} \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
10	8 9	syl	$⊢ (r = T \land i = I) \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
11	10 2	eqtr4di	$⊢ (r = T \land i = I) \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = D$
12	11	sseq2d	$⊢ (r = T \land i = I) \to (\{x, y\} \subseteq \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} \leftrightarrow \{x, y\} \subseteq D)$
13		simpl	$⊢ (r = T \land i = I) \to r = T$
14	13	breqd	$⊢ (r = T \land i = I) \to (z r w \leftrightarrow z T w)$
15	14	imbi1d	$⊢ (r = T \land i = I) \to ((z r w \to x (w) = y (w)) \leftrightarrow (z T w \to x (w) = y (w)))$
16	7 15	raleqbidv	$⊢ (r = T \land i = I) \to (\forall w \in i (z r w \to x (w) = y (w)) \leftrightarrow \forall w \in I (z T w \to x (w) = y (w)))$
17	16	anbi2d	$⊢ (r = T \land i = I) \to ((x (z) < y (z) \land \forall w \in i (z r w \to x (w) = y (w))) \leftrightarrow (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))$
18	7 17	rexeqbidv	$⊢ (r = T \land i = I) \to (\exists z \in i (x (z) < y (z) \land \forall w \in i (z r w \to x (w) = y (w))) \leftrightarrow \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))$
19	12 18	anbi12d	$⊢ (r = T \land i = I) \to ((\{x, y\} \subseteq \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} \land \exists z \in i (x (z) < y (z) \land \forall w \in i (z r w \to x (w) = y (w)))) \leftrightarrow (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))))$
20	19	opabbidv	$⊢ (r = T \land i = I) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} \land \exists z \in i (x (z) < y (z) \land \forall w \in i (z r w \to x (w) = y (w))))\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\}$
21		df-ltbag	$⊢ <_{bag} = (r \in V, i \in V ⟼ \{⟨x, y⟩ \| (\{x, y\} \subseteq \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} \land \exists z \in i (x (z) < y (z) \land \forall w \in i (z r w \to x (w) = y (w))))\})$
22		vex	$⊢ x \in V$
23		vex	$⊢ y \in V$
24	22 23	prss	$⊢ (x \in D \land y \in D) \leftrightarrow \{x, y\} \subseteq D$
25	24	anbi1i	$⊢ ((x \in D \land y \in D) \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))) \leftrightarrow (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))$
26	25	opabbii	$⊢ \{⟨x, y⟩ \| ((x \in D \land y \in D) \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\}$
27		ovex	$⊢ {ℕ_{0}}^{I} \in V$
28	2 27	rabex2	$⊢ D \in V$
29	28 28	xpex	$⊢ D \times D \in V$
30		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in D \land y \in D) \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\} \subseteq D \times D$
31	29 30	ssexi	$⊢ \{⟨x, y⟩ \| ((x \in D \land y \in D) \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\} \in V$
32	26 31	eqeltrri	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\} \in V$
33	20 21 32	ovmpoa	$⊢ (T \in V \land I \in V) \to T <_{bag} I = \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\}$
34	5 6 33	syl2an	$⊢ (T \in W \land I \in V) \to T <_{bag} I = \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\}$
35	4 3 34	syl2anc	$⊢ φ \to T <_{bag} I = \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\}$
36	1 35	syl5eq	$⊢ φ \to C = \{⟨x, y⟩ \| (\{x, y\} \subseteq D \land \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w))))\}$

Metamath Proof Explorer

Theorem ltbval

Proof