ltbwe

Description: The finite bag order is a well-order, given a well-order of the index set. (Contributed by Mario Carneiro, 2-Jun-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$
	ltbwe.w	$⊢ φ \to T We I$
Assertion	ltbwe	$⊢ φ \to C We D$

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		ltbwe.w	$⊢ φ \to T We I$
6		eqid	$⊢ \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} = \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\}$
7		breq1	$⊢ h = x \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (x))$
8	7	cbvrabv	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{x \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (x)\}$
9		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
10		ltweuz	$⊢ < We ℤ_{\geq 0}$
11		weeq2	$⊢ ℕ_{0} = ℤ_{\geq 0} \to (< We ℕ_{0} \leftrightarrow < We ℤ_{\geq 0})$
12	10 11	mpbiri	$⊢ ℕ_{0} = ℤ_{\geq 0} \to < We ℕ_{0}$
13	9 12	mp1i	$⊢ φ \to < We ℕ_{0}$
14		0nn0	$⊢ 0 \in ℕ_{0}$
15		ne0i	$⊢ 0 \in ℕ_{0} \to ℕ_{0} \neq \emptyset$
16	14 15	mp1i	$⊢ φ \to ℕ_{0} \neq \emptyset$
17		eqid	$⊢ OrdIso (T, I) = OrdIso (T, I)$
18		0z	$⊢ 0 \in ℤ$
19		hashgval2	$⊢ {\|.\| ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
20	18 19	om2uzoi	$⊢ {\|.\| ↾}_{ω} = OrdIso (< ℤ_{\geq 0})$
21		oieq2	$⊢ ℕ_{0} = ℤ_{\geq 0} \to OrdIso (< ℕ_{0}) = OrdIso (< ℤ_{\geq 0})$
22	9 21	ax-mp	$⊢ OrdIso (< ℕ_{0}) = OrdIso (< ℤ_{\geq 0})$
23	20 22	eqtr4i	$⊢ {\|.\| ↾}_{ω} = OrdIso (< ℕ_{0})$
24		peano1	$⊢ \emptyset \in ω$
25		fvres	$⊢ \emptyset \in ω \to ({\|.\| ↾}_{ω}) (\emptyset) = \|\emptyset\|$
26	24 25	ax-mp	$⊢ ({\|.\| ↾}_{ω}) (\emptyset) = \|\emptyset\|$
27		hash0	$⊢ \|\emptyset\| = 0$
28	26 27	eqtr2i	$⊢ 0 = ({\|.\| ↾}_{ω}) (\emptyset)$
29	6 8 5 13 16 17 23 28	wemapwe	$⊢ φ \to \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} We \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
30		elmapfun	$⊢ h \in ({ℕ_{0}}^{I}) \to Fun h$
31	30	adantl	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to Fun h$
32		simpr	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to h \in ({ℕ_{0}}^{I})$
33		c0ex	$⊢ 0 \in V$
34	33	a1i	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to 0 \in V$
35		funisfsupp	$⊢ (Fun h \land h \in ({ℕ_{0}}^{I}) \land 0 \in V) \to ({finSupp}_{0} (h) \leftrightarrow h supp 0 \in Fin)$
36	31 32 34 35	syl3anc	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to ({finSupp}_{0} (h) \leftrightarrow h supp 0 \in Fin)$
37		elmapi	$⊢ h \in ({ℕ_{0}}^{I}) \to h : I ⟶ ℕ_{0}$
38		frnnn0supp	$⊢ (I \in V \land h : I ⟶ ℕ_{0}) \to h supp 0 = h^{-1} [ℕ]$
39	38	eleq1d	$⊢ (I \in V \land h : I ⟶ ℕ_{0}) \to (h supp 0 \in Fin \leftrightarrow h^{-1} [ℕ] \in Fin)$
40	3 37 39	syl2an	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to (h supp 0 \in Fin \leftrightarrow h^{-1} [ℕ] \in Fin)$
41	36 40	bitr2d	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to (h^{-1} [ℕ] \in Fin \leftrightarrow {finSupp}_{0} (h))$
42	41	rabbidva	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
43	2 42	syl5eq	$⊢ φ \to D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
44		weeq2	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \to (\{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} We D \leftrightarrow \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} We \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\})$
45	43 44	syl	$⊢ φ \to (\{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} We D \leftrightarrow \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} We \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\})$
46	29 45	mpbird	$⊢ φ \to \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} We D$
47		weinxp	$⊢ \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} We D \leftrightarrow (\{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D)) We D$
48	46 47	sylib	$⊢ φ \to (\{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D)) We D$
49	1 2 3 4	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))))\}$
50		df-xp	$⊢ D \times D = \{⟨x, y⟩ \| (x \in D \land y \in D)\}$
51		vex	$⊢ x \in V$
52		vex	$⊢ y \in V$
53	51 52	prss	$⊢ (x \in D \land y \in D) \leftrightarrow \{x, y\} \subseteq D$
54	53	opabbii	$⊢ \{⟨x, y⟩ \| (x \in D \land y \in D)\} = \{⟨x, y⟩ \| \{x, y\} \subseteq D\}$
55	50 54	eqtr2i	$⊢ \{⟨x, y⟩ \| \{x, y\} \subseteq D\} = D \times D$
56	55	ineq1i	$⊢ \{⟨x, y⟩ \| \{x, y\} \subseteq D\} \cap \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} = (D \times D) \cap \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\}$
57		inopab	$⊢ \{⟨x, y⟩ \| \{x, y\} \subseteq D\} \cap \{⟨x, y⟩ \| \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))))\}$
58		incom	$⊢ (D \times D) \cap \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} = \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D)$
59	56 57 58	3eqtr3i	$⊢ \{⟨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))))\} = \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D)$
60	49 59	eqtrdi	$⊢ φ \to C = \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D)$
61		weeq1	$⊢ C = \{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D) \to (C We D \leftrightarrow (\{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D)) We D)$
62	60 61	syl	$⊢ φ \to (C We D \leftrightarrow (\{⟨x, y⟩ \| \exists z \in I (x (z) < y (z) \land \forall w \in I (z T w \to x (w) = y (w)))\} \cap (D \times D)) We D)$
63	48 62	mpbird	$⊢ φ \to C We D$

Metamath Proof Explorer

Theorem ltbwe

Proof