Theorem unxpwdom3 43544

Description: Weaker version of unxpwdom 9498 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 7699	. 2 ⊢ (𝜑 → (𝐷 × 𝐵) ∈ V)
4		simprr 773	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (𝑎 + 𝑑) ∈ 𝐵)
5		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 ∈ 𝐶)
6		unxpwdom3.rc	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
7	6	an4s 661	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
8	7	anassrs 467	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑑 ∈ 𝐷) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
9	8	adantlrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
10	5, 9	riota5 7347	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)) = 𝑎)
11	10	eqcomd 2743	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
12		eqeq2 2749	. . . . . . 7 ⊢ (𝑦 = (𝑎 + 𝑑) → ((𝑐 + 𝑑) = 𝑦 ↔ (𝑐 + 𝑑) = (𝑎 + 𝑑)))
13	12	riotabidv 7320	. . . . . 6 ⊢ (𝑦 = (𝑎 + 𝑑) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
14	13	rspceeqv 3588	. . . . 5 ⊢ (((𝑎 + 𝑑) ∈ 𝐵 ∧ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
15	4, 11, 14	syl2anc 585	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
16		unxpwdom3.ni	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)
17	16	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ 𝐷 ≼ 𝐴)
18		unxpwdom3.av	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
19	18	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐴 ∈ 𝑉)
20		oveq2 7369	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑏 → (𝑎 + 𝑑) = (𝑎 + 𝑏))
21	20	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑏 → ((𝑎 + 𝑑) ∈ 𝐵 ↔ (𝑎 + 𝑏) ∈ 𝐵))
22	21	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑏 → (¬ (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ (𝑎 + 𝑏) ∈ 𝐵))
23	22	rspcv 3561	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐷 → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
24	23	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
25		unxpwdom3.ov	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
26	25	3expa 1119	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
27		elun 4094	. . . . . . . . . . . . 13 ⊢ ((𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵) ↔ ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
28	26, 27	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
29	28	orcomd 872	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐵 ∨ (𝑎 + 𝑏) ∈ 𝐴))
30	29	ord 865	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (¬ (𝑎 + 𝑏) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴))
31	24, 30	syld 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴))
32	31	impancom 451	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝑏 ∈ 𝐷 → (𝑎 + 𝑏) ∈ 𝐴))
33		unxpwdom3.lc	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))
34	33	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)))
35	34	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)))
36	32, 35	dom2d 8934	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴))
37	19, 36	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐷 ≼ 𝐴)
38	17, 37	mtand 816	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
39		dfrex2 3065	. . . . 5 ⊢ (∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
40	38, 39	sylibr 234	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵)
41	15, 40	reximddv 3154	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
42		vex 3434	. . . . . . . . 9 ⊢ 𝑑 ∈ V
43		vex 3434	. . . . . . . . 9 ⊢ 𝑦 ∈ V
44	42, 43	op1std 7946	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (1st ‘𝑥) = 𝑑)
45	44	oveq2d 7377	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑐 + (1st ‘𝑥)) = (𝑐 + 𝑑))
46	42, 43	op2ndd 7947	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (2nd ‘𝑥) = 𝑦)
47	45, 46	eqeq12d 2753	. . . . . 6 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → ((𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥) ↔ (𝑐 + 𝑑) = 𝑦))
48	47	riotabidv 7320	. . . . 5 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
49	48	eqeq2d 2748	. . . 4 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)))
50	49	rexxp 5792	. . 3 ⊢ (∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
51	41, 50	sylibr 234	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)))
52	3, 51	wdomd 9490	1 ⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ∪ cun 3888  ⟨cop 4574   class class class wbr 5086   × cxp 5623  ‘cfv 6493  ℩crio 7317  (class class class)co 7361  1^st c1st 7934  2^nd c2nd 7935   ≼ cdom 8885   ≼^* cwdom 9473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-1st 7936  df-2nd 7937  df-en 8888  df-dom 8889  df-sdom 8890  df-wdom 9474

This theorem is referenced by:  isnumbasgrplem2  43553