Theorem unxpwdom3 44363

Description: Weaker version of unxpwdom 9620 where a function is required only to be cancellative, not an injection. 𝐷 and 𝐵 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 𝐴, each row must hit an element of 𝐵; by column injectivity, each row can be identified in at least one way by the 𝐵 element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE

Hypotheses

Ref	Expression
unxpwdom3.av	⊢ (𝜑 → 𝐴 ∈ 𝑉)
unxpwdom3.bv	⊢ (𝜑 → 𝐵 ∈ 𝑊)
unxpwdom3.dv	⊢ (𝜑 → 𝐷 ∈ 𝑋)
unxpwdom3.ov	⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
unxpwdom3.lc	⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))
unxpwdom3.rc	⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
unxpwdom3.ni	⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)

Assertion

Ref	Expression
unxpwdom3	⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝐵   𝐶,𝑎,𝑏,𝑐,𝑑   𝐷,𝑎,𝑏,𝑐,𝑑   + ,𝑎,𝑏,𝑐,𝑑   𝜑,𝑎,𝑏,𝑐,𝑑   𝐴,𝑏,𝑐

Allowed substitution hints:   𝐴(𝑎, 𝑑)   𝑉(𝑎, 𝑏, 𝑐, 𝑑)   𝑊(𝑎, 𝑏, 𝑐, 𝑑)   𝑋(𝑎, 𝑏, 𝑐, 𝑑)

Proof of Theorem unxpwdom3

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unxpwdom3.dv	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
2		unxpwdom3.bv	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3	1, 2	xpexd 7797	. 2 ⊢ (𝜑 → (𝐷 × 𝐵) ∈ V)
4		simprr 785	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (𝑎 + 𝑑) ∈ 𝐵)
5		simplr 781	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 ∈ 𝐶)
6		unxpwdom3.rc	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
7	6	an4s 673	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
8	7	anassrs 473	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑑 ∈ 𝐷) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
9	8	adantlrr 734	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
10	5, 9	riota5 7437	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)) = 𝑎)
11	10	eqcomd 2769	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
12		eqeq2 2775	. . . . . . 7 ⊢ (𝑦 = (𝑎 + 𝑑) → ((𝑐 + 𝑑) = 𝑦 ↔ (𝑐 + 𝑑) = (𝑎 + 𝑑)))
13	12	riotabidv 7410	. . . . . 6 ⊢ (𝑦 = (𝑎 + 𝑑) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
14	13	rspceeqv 3602	. . . . 5 ⊢ (((𝑎 + 𝑑) ∈ 𝐵 ∧ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
15	4, 11, 14	syl2anc 596	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
16		unxpwdom3.ni	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)
17	16	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ 𝐷 ≼ 𝐴)
18		unxpwdom3.av	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
19	18	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐴 ∈ 𝑉)
20		oveq2 7459	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑏 → (𝑎 + 𝑑) = (𝑎 + 𝑏))
21	20	eleq1d 2849	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑏 → ((𝑎 + 𝑑) ∈ 𝐵 ↔ (𝑎 + 𝑏) ∈ 𝐵))
22	21	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑏 → (¬ (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ (𝑎 + 𝑏) ∈ 𝐵))
23	22	rspcv 3576	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐷 → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
24	23	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
25		unxpwdom3.ov	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
26	25	3expa 1136	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
27		elun 4155	. . . . . . . . . . . . 13 ⊢ ((𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵) ↔ ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
28	26, 27	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
29	28	orcomd 885	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐵 ∨ (𝑎 + 𝑏) ∈ 𝐴))
30	29	ord 878	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (¬ (𝑎 + 𝑏) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴))
31	24, 30	syld 48	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴))
32	31	impancom 457	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝑏 ∈ 𝐷 → (𝑎 + 𝑏) ∈ 𝐴))
33		unxpwdom3.lc	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))
34	33	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)))
35	34	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)))
36	32, 35	dom2d 9058	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴))
37	19, 36	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐷 ≼ 𝐴)
38	17, 37	mtand 828	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
39		dfrex2 3093	. . . . 5 ⊢ (∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
40	38, 39	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵)
41	15, 40	reximddv 3182	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
42		vex 3458	. . . . . . . . 9 ⊢ 𝑑 ∈ V
43		vex 3458	. . . . . . . . 9 ⊢ 𝑦 ∈ V
44	42, 43	op1std 8045	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (1st ‘𝑥) = 𝑑)
45	44	oveq2d 7467	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑐 + (1st ‘𝑥)) = (𝑐 + 𝑑))
46	42, 43	op2ndd 8046	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (2nd ‘𝑥) = 𝑦)
47	45, 46	eqeq12d 2779	. . . . . 6 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → ((𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥) ↔ (𝑐 + 𝑑) = 𝑦))
48	47	riotabidv 7410	. . . . 5 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
49	48	eqeq2d 2774	. . . 4 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)))
50	49	rexxp 5829	. . 3 ⊢ (∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
51	41, 50	sylibr 237	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)))
52	3, 51	wdomd 9612	1 ⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ∪ cun 4152  ⟨cop 4840   class class class wbr 5108   × cxp 5656  ‘cfv 6566  ℩crio 7407  (class class class)co 7451  1^st c1st 8033  2^nd c2nd 8034   ≼ cdom 9009   ≼^* cwdom 9595

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-1st 8035  df-2nd 8036  df-en 9012  df-dom 9013  df-sdom 9014  df-wdom 9596

This theorem is used by:  isnumbasgrplem2  44371