unxpwdom3

Description: Weaker version of unxpwdom where a function is required only to be cancellative, not an injection. D and B are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into A , each row must hit an element of B ; by column injectivity, each row can be identified in at least one way by the B element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015)MOVABLE

	Ref	Expression
Hypotheses	unxpwdom3.av	$⊢ φ \to A \in V$
	unxpwdom3.bv	$⊢ φ \to B \in W$
	unxpwdom3.dv	$⊢ φ \to D \in X$
	unxpwdom3.ov	$⊢ (φ \land a \in C \land b \in D) \to a \underset{˙}{+} b \in (A \cup B)$
	unxpwdom3.lc	$⊢ ((φ \land a \in C) \land (b \in D \land c \in D)) \to (a \underset{˙}{+} b = a \underset{˙}{+} c \leftrightarrow b = c)$
	unxpwdom3.rc	$⊢ ((φ \land d \in D) \land (a \in C \land c \in C)) \to (c \underset{˙}{+} d = a \underset{˙}{+} d \leftrightarrow c = a)$
	unxpwdom3.ni	$⊢ φ \to \neg D ≼ A$
Assertion	unxpwdom3	$⊢ φ \to C ≼^{*} (D \times B)$

Proof

Step	Hyp	Ref	Expression
1		unxpwdom3.av	$⊢ φ \to A \in V$
2		unxpwdom3.bv	$⊢ φ \to B \in W$
3		unxpwdom3.dv	$⊢ φ \to D \in X$
4		unxpwdom3.ov	$⊢ (φ \land a \in C \land b \in D) \to a \underset{˙}{+} b \in (A \cup B)$
5		unxpwdom3.lc	$⊢ ((φ \land a \in C) \land (b \in D \land c \in D)) \to (a \underset{˙}{+} b = a \underset{˙}{+} c \leftrightarrow b = c)$
6		unxpwdom3.rc	$⊢ ((φ \land d \in D) \land (a \in C \land c \in C)) \to (c \underset{˙}{+} d = a \underset{˙}{+} d \leftrightarrow c = a)$
7		unxpwdom3.ni	$⊢ φ \to \neg D ≼ A$
8	3 2	xpexd	$⊢ φ \to D \times B \in V$
9		simprr	$⊢ ((φ \land a \in C) \land (d \in D \land a \underset{˙}{+} d \in B)) \to a \underset{˙}{+} d \in B$
10		simplr	$⊢ ((φ \land a \in C) \land (d \in D \land a \underset{˙}{+} d \in B)) \to a \in C$
11	6	an4s	$⊢ ((φ \land a \in C) \land (d \in D \land c \in C)) \to (c \underset{˙}{+} d = a \underset{˙}{+} d \leftrightarrow c = a)$
12	11	anassrs	$⊢ (((φ \land a \in C) \land d \in D) \land c \in C) \to (c \underset{˙}{+} d = a \underset{˙}{+} d \leftrightarrow c = a)$
13	12	adantlrr	$⊢ (((φ \land a \in C) \land (d \in D \land a \underset{˙}{+} d \in B)) \land c \in C) \to (c \underset{˙}{+} d = a \underset{˙}{+} d \leftrightarrow c = a)$
14	10 13	riota5	$⊢ ((φ \land a \in C) \land (d \in D \land a \underset{˙}{+} d \in B)) \to (ι c \in C \| c \underset{˙}{+} d = a \underset{˙}{+} d) = a$
15	14	eqcomd	$⊢ ((φ \land a \in C) \land (d \in D \land a \underset{˙}{+} d \in B)) \to a = (ι c \in C \| c \underset{˙}{+} d = a \underset{˙}{+} d)$
16		eqeq2	$⊢ y = a \underset{˙}{+} d \to (c \underset{˙}{+} d = y \leftrightarrow c \underset{˙}{+} d = a \underset{˙}{+} d)$
17	16	riotabidv	$⊢ y = a \underset{˙}{+} d \to (ι c \in C \| c \underset{˙}{+} d = y) = (ι c \in C \| c \underset{˙}{+} d = a \underset{˙}{+} d)$
18	17	rspceeqv	$⊢ (a \underset{˙}{+} d \in B \land a = (ι c \in C \| c \underset{˙}{+} d = a \underset{˙}{+} d)) \to \exists y \in B a = (ι c \in C \| c \underset{˙}{+} d = y)$
19	9 15 18	syl2anc	$⊢ ((φ \land a \in C) \land (d \in D \land a \underset{˙}{+} d \in B)) \to \exists y \in B a = (ι c \in C \| c \underset{˙}{+} d = y)$
20	7	adantr	$⊢ (φ \land a \in C) \to \neg D ≼ A$
21	1	ad2antrr	$⊢ ((φ \land a \in C) \land \forall d \in D \neg a \underset{˙}{+} d \in B) \to A \in V$
22		oveq2	$⊢ d = b \to a \underset{˙}{+} d = a \underset{˙}{+} b$
23	22	eleq1d	$⊢ d = b \to (a \underset{˙}{+} d \in B \leftrightarrow a \underset{˙}{+} b \in B)$
24	23	notbid	$⊢ d = b \to (\neg a \underset{˙}{+} d \in B \leftrightarrow \neg a \underset{˙}{+} b \in B)$
25	24	rspcv	$⊢ b \in D \to (\forall d \in D \neg a \underset{˙}{+} d \in B \to \neg a \underset{˙}{+} b \in B)$
26	25	adantl	$⊢ ((φ \land a \in C) \land b \in D) \to (\forall d \in D \neg a \underset{˙}{+} d \in B \to \neg a \underset{˙}{+} b \in B)$
27	4	3expa	$⊢ ((φ \land a \in C) \land b \in D) \to a \underset{˙}{+} b \in (A \cup B)$
28		elun	$⊢ a \underset{˙}{+} b \in (A \cup B) \leftrightarrow (a \underset{˙}{+} b \in A \lor a \underset{˙}{+} b \in B)$
29	27 28	sylib	$⊢ ((φ \land a \in C) \land b \in D) \to (a \underset{˙}{+} b \in A \lor a \underset{˙}{+} b \in B)$
30	29	orcomd	$⊢ ((φ \land a \in C) \land b \in D) \to (a \underset{˙}{+} b \in B \lor a \underset{˙}{+} b \in A)$
31	30	ord	$⊢ ((φ \land a \in C) \land b \in D) \to (\neg a \underset{˙}{+} b \in B \to a \underset{˙}{+} b \in A)$
32	26 31	syld	$⊢ ((φ \land a \in C) \land b \in D) \to (\forall d \in D \neg a \underset{˙}{+} d \in B \to a \underset{˙}{+} b \in A)$
33	32	impancom	$⊢ ((φ \land a \in C) \land \forall d \in D \neg a \underset{˙}{+} d \in B) \to (b \in D \to a \underset{˙}{+} b \in A)$
34	5	ex	$⊢ (φ \land a \in C) \to ((b \in D \land c \in D) \to (a \underset{˙}{+} b = a \underset{˙}{+} c \leftrightarrow b = c))$
35	34	adantr	$⊢ ((φ \land a \in C) \land \forall d \in D \neg a \underset{˙}{+} d \in B) \to ((b \in D \land c \in D) \to (a \underset{˙}{+} b = a \underset{˙}{+} c \leftrightarrow b = c))$
36	33 35	dom2d	$⊢ ((φ \land a \in C) \land \forall d \in D \neg a \underset{˙}{+} d \in B) \to (A \in V \to D ≼ A)$
37	21 36	mpd	$⊢ ((φ \land a \in C) \land \forall d \in D \neg a \underset{˙}{+} d \in B) \to D ≼ A$
38	20 37	mtand	$⊢ (φ \land a \in C) \to \neg \forall d \in D \neg a \underset{˙}{+} d \in B$
39		dfrex2	$⊢ \exists d \in D a \underset{˙}{+} d \in B \leftrightarrow \neg \forall d \in D \neg a \underset{˙}{+} d \in B$
40	38 39	sylibr	$⊢ (φ \land a \in C) \to \exists d \in D a \underset{˙}{+} d \in B$
41	19 40	reximddv	$⊢ (φ \land a \in C) \to \exists d \in D \exists y \in B a = (ι c \in C \| c \underset{˙}{+} d = y)$
42		vex	$⊢ d \in V$
43		vex	$⊢ y \in V$
44	42 43	op1std	$⊢ x = ⟨d, y⟩ \to 1^{st} (x) = d$
45	44	oveq2d	$⊢ x = ⟨d, y⟩ \to c \underset{˙}{+} 1^{st} (x) = c \underset{˙}{+} d$
46	42 43	op2ndd	$⊢ x = ⟨d, y⟩ \to 2^{nd} (x) = y$
47	45 46	eqeq12d	$⊢ x = ⟨d, y⟩ \to (c \underset{˙}{+} 1^{st} (x) = 2^{nd} (x) \leftrightarrow c \underset{˙}{+} d = y)$
48	47	riotabidv	$⊢ x = ⟨d, y⟩ \to (ι c \in C \| c \underset{˙}{+} 1^{st} (x) = 2^{nd} (x)) = (ι c \in C \| c \underset{˙}{+} d = y)$
49	48	eqeq2d	$⊢ x = ⟨d, y⟩ \to (a = (ι c \in C \| c \underset{˙}{+} 1^{st} (x) = 2^{nd} (x)) \leftrightarrow a = (ι c \in C \| c \underset{˙}{+} d = y))$
50	49	rexxp	$⊢ \exists x \in (D \times B) a = (ι c \in C \| c \underset{˙}{+} 1^{st} (x) = 2^{nd} (x)) \leftrightarrow \exists d \in D \exists y \in B a = (ι c \in C \| c \underset{˙}{+} d = y)$
51	41 50	sylibr	$⊢ (φ \land a \in C) \to \exists x \in (D \times B) a = (ι c \in C \| c \underset{˙}{+} 1^{st} (x) = 2^{nd} (x))$
52	8 51	wdomd	$⊢ φ \to C ≼^{*} (D \times B)$

Metamath Proof Explorer

Theorem unxpwdom3

Proof