oemapso

Description: The relation T is a strict order on S (a corollary of wemapso2 ). (Contributed by Mario Carneiro, 28-May-2015)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
Assertion	oemapso	$⊢ φ \to T Or S$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
5		eloni	$⊢ B \in On \to Ord B$
6		ordwe	$⊢ Ord B \to E We B$
7		weso	$⊢ E We B \to E Or B$
8	3 5 6 7	4syl	$⊢ φ \to E Or B$
9		cnvso	$⊢ E Or B \leftrightarrow E^{-1} Or B$
10	8 9	sylib	$⊢ φ \to E^{-1} Or B$
11		eloni	$⊢ A \in On \to Ord A$
12		ordwe	$⊢ Ord A \to E We A$
13		weso	$⊢ E We A \to E Or A$
14	2 11 12 13	4syl	$⊢ φ \to E Or A$
15		fvex	$⊢ y (z) \in V$
16	15	epeli	$⊢ x (z) E y (z) \leftrightarrow x (z) \in y (z)$
17		vex	$⊢ w \in V$
18		vex	$⊢ z \in V$
19	17 18	brcnv	$⊢ w E^{-1} z \leftrightarrow z E w$
20		epel	$⊢ z E w \leftrightarrow z \in w$
21	19 20	bitri	$⊢ w E^{-1} z \leftrightarrow z \in w$
22	21	imbi1i	$⊢ (w E^{-1} z \to x (w) = y (w)) \leftrightarrow (z \in w \to x (w) = y (w))$
23	22	ralbii	$⊢ \forall w \in B (w E^{-1} z \to x (w) = y (w)) \leftrightarrow \forall w \in B (z \in w \to x (w) = y (w))$
24	16 23	anbi12i	$⊢ (x (z) E y (z) \land \forall w \in B (w E^{-1} z \to x (w) = y (w))) \leftrightarrow (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))$
25	24	rexbii	$⊢ \exists z \in B (x (z) E y (z) \land \forall w \in B (w E^{-1} z \to x (w) = y (w))) \leftrightarrow \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))$
26	25	opabbii	$⊢ \{⟨x, y⟩ \| \exists z \in B (x (z) E y (z) \land \forall w \in B (w E^{-1} z \to x (w) = y (w)))\} = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
27	4 26	eqtr4i	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) E y (z) \land \forall w \in B (w E^{-1} z \to x (w) = y (w)))\}$
28		breq1	$⊢ g = x \to ({finSupp}_{\emptyset} (g) \leftrightarrow {finSupp}_{\emptyset} (x))$
29	28	cbvrabv	$⊢ \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} = \{x \in (A^{B}) \| {finSupp}_{\emptyset} (x)\}$
30	27 29	wemapso2	$⊢ (B \in On \land E^{-1} Or B \land E Or A) \to T Or \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
31	3 10 14 30	syl3anc	$⊢ φ \to T Or \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
32		eqid	$⊢ \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
33	32 2 3	cantnfdm	$⊢ φ \to dom (A CNF B) = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
34	1 33	syl5eq	$⊢ φ \to S = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
35		soeq2	$⊢ S = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} \to (T Or S \leftrightarrow T Or \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\})$
36	34 35	syl	$⊢ φ \to (T Or S \leftrightarrow T Or \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\})$
37	31 36	mpbird	$⊢ φ \to T Or S$

Metamath Proof Explorer

Theorem oemapso

Proof