Theorem unxpwdom3 43083

Description: Weaker version of unxpwdom 9626 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 7769	. 2 ⊢ (𝜑 → (𝐷 × 𝐵) ∈ V)
4		simprr 773	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (𝑎 + 𝑑) ∈ 𝐵)
5		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 ∈ 𝐶)
6		unxpwdom3.rc	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
7	6	an4s 660	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
8	7	anassrs 467	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑑 ∈ 𝐷) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
9	8	adantlrr 721	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
10	5, 9	riota5 7416	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)) = 𝑎)
11	10	eqcomd 2740	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
12		eqeq2 2746	. . . . . . 7 ⊢ (𝑦 = (𝑎 + 𝑑) → ((𝑐 + 𝑑) = 𝑦 ↔ (𝑐 + 𝑑) = (𝑎 + 𝑑)))
13	12	riotabidv 7389	. . . . . 6 ⊢ (𝑦 = (𝑎 + 𝑑) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
14	13	rspceeqv 3644	. . . . 5 ⊢ (((𝑎 + 𝑑) ∈ 𝐵 ∧ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
15	4, 11, 14	syl2anc 584	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
16		unxpwdom3.ni	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)
17	16	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ 𝐷 ≼ 𝐴)
18		unxpwdom3.av	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
19	18	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐴 ∈ 𝑉)
20		oveq2 7438	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑏 → (𝑎 + 𝑑) = (𝑎 + 𝑏))
21	20	eleq1d 2823	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑏 → ((𝑎 + 𝑑) ∈ 𝐵 ↔ (𝑎 + 𝑏) ∈ 𝐵))
22	21	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑏 → (¬ (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ (𝑎 + 𝑏) ∈ 𝐵))
23	22	rspcv 3617	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐷 → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
24	23	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
25		unxpwdom3.ov	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
26	25	3expa 1117	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
27		elun 4162	. . . . . . . . . . . . 13 ⊢ ((𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵) ↔ ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
28	26, 27	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
29	28	orcomd 871	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐵 ∨ (𝑎 + 𝑏) ∈ 𝐴))
30	29	ord 864	. . . . . . . . . 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 9031	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴))
37	19, 36	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐷 ≼ 𝐴)
38	17, 37	mtand 816	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
39		dfrex2 3070	. . . . 5 ⊢ (∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
40	38, 39	sylibr 234	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵)
41	15, 40	reximddv 3168	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
42		vex 3481	. . . . . . . . 9 ⊢ 𝑑 ∈ V
43		vex 3481	. . . . . . . . 9 ⊢ 𝑦 ∈ V
44	42, 43	op1std 8022	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (1st ‘𝑥) = 𝑑)
45	44	oveq2d 7446	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑐 + (1st ‘𝑥)) = (𝑐 + 𝑑))
46	42, 43	op2ndd 8023	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (2nd ‘𝑥) = 𝑦)
47	45, 46	eqeq12d 2750	. . . . . 6 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → ((𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥) ↔ (𝑐 + 𝑑) = 𝑦))
48	47	riotabidv 7389	. . . . 5 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
49	48	eqeq2d 2745	. . . 4 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)))
50	49	rexxp 5855	. . 3 ⊢ (∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
51	41, 50	sylibr 234	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)))
52	3, 51	wdomd 9618	1 ⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ∀wral 3058  ∃wrex 3067  Vcvv 3477   ∪ cun 3960  ⟨cop 4636   class class class wbr 5147   × cxp 5686  ‘cfv 6562  ℩crio 7386  (class class class)co 7430  1^st c1st 8010  2^nd c2nd 8011   ≼ cdom 8981   ≼^* cwdom 9601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-1st 8012  df-2nd 8013  df-en 8984  df-dom 8985  df-sdom 8986  df-wdom 9602

This theorem is referenced by:  isnumbasgrplem2  43092