Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
unxpwdom3.bv ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
unxpwdom3.dv ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
unxpwdom3.ov ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑎 + 𝑏 ) ∈ ( 𝐴 ∪ 𝐵 ) )
unxpwdom3.lc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷 ) ) → ( ( 𝑎 + 𝑏 ) = ( 𝑎 + 𝑐 ) ↔ 𝑏 = 𝑐 ) )
unxpwdom3.rc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ↔ 𝑐 = 𝑎 ) )
unxpwdom3.ni ⊢ ( 𝜑 → ¬ 𝐷 ≼ 𝐴 )
Assertion unxpwdom3 ( 𝜑 → 𝐶 ≼* ( 𝐷 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 unxpwdom3.av ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 unxpwdom3.bv ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 unxpwdom3.dv ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
4 unxpwdom3.ov ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑎 + 𝑏 ) ∈ ( 𝐴 ∪ 𝐵 ) )
5 unxpwdom3.lc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷 ) ) → ( ( 𝑎 + 𝑏 ) = ( 𝑎 + 𝑐 ) ↔ 𝑏 = 𝑐 ) )
6 unxpwdom3.rc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ↔ 𝑐 = 𝑎 ) )
7 unxpwdom3.ni ⊢ ( 𝜑 → ¬ 𝐷 ≼ 𝐴 )
8 3 2 xpexd ⊢ ( 𝜑 → ( 𝐷 × 𝐵 ) ∈ V )
9 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ∧ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) ) → ( 𝑎 + 𝑑 ) ∈ 𝐵 )
10 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ∧ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) ) → 𝑎 ∈ 𝐶 )
11 6 an4s ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ↔ 𝑐 = 𝑎 ) )
12 11 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ 𝑑 ∈ 𝐷 ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ↔ 𝑐 = 𝑎 ) )
13 12 adantlrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ∧ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ↔ 𝑐 = 𝑎 ) )
14 10 13 riota5 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ∧ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) ) → ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ) = 𝑎 )
15 14 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ∧ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) ) → 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ) )
16 eqeq2 ⊢ ( 𝑦 = ( 𝑎 + 𝑑 ) → ( ( 𝑐 + 𝑑 ) = 𝑦 ↔ ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ) )
17 16 riotabidv ⊢ ( 𝑦 = ( 𝑎 + 𝑑 ) → ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = 𝑦 ) = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ) )
18 17 rspceeqv ⊢ ( ( ( 𝑎 + 𝑑 ) ∈ 𝐵 ∧ 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = ( 𝑎 + 𝑑 ) ) ) → ∃ 𝑦 ∈ 𝐵 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = 𝑦 ) )
19 9 15 18 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ∧ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) ) → ∃ 𝑦 ∈ 𝐵 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = 𝑦 ) )
20 7 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ¬ 𝐷 ≼ 𝐴 )
21 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) → 𝐴 ∈ 𝑉 )
22 oveq2 ⊢ ( 𝑑 = 𝑏 → ( 𝑎 + 𝑑 ) = ( 𝑎 + 𝑏 ) )
23 22 eleq1d ⊢ ( 𝑑 = 𝑏 → ( ( 𝑎 + 𝑑 ) ∈ 𝐵 ↔ ( 𝑎 + 𝑏 ) ∈ 𝐵 ) )
24 23 notbid ⊢ ( 𝑑 = 𝑏 → ( ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 ↔ ¬ ( 𝑎 + 𝑏 ) ∈ 𝐵 ) )
25 24 rspcv ⊢ ( 𝑏 ∈ 𝐷 → ( ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 → ¬ ( 𝑎 + 𝑏 ) ∈ 𝐵 ) )
26 25 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐷 ) → ( ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 → ¬ ( 𝑎 + 𝑏 ) ∈ 𝐵 ) )
27 4 3expa ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐷 ) → ( 𝑎 + 𝑏 ) ∈ ( 𝐴 ∪ 𝐵 ) )
28 elun ⊢ ( ( 𝑎 + 𝑏 ) ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( ( 𝑎 + 𝑏 ) ∈ 𝐴 ∨ ( 𝑎 + 𝑏 ) ∈ 𝐵 ) )
29 27 28 sylib ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑎 + 𝑏 ) ∈ 𝐴 ∨ ( 𝑎 + 𝑏 ) ∈ 𝐵 ) )
30 29 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑎 + 𝑏 ) ∈ 𝐵 ∨ ( 𝑎 + 𝑏 ) ∈ 𝐴 ) )
31 30 ord ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐷 ) → ( ¬ ( 𝑎 + 𝑏 ) ∈ 𝐵 → ( 𝑎 + 𝑏 ) ∈ 𝐴 ) )
32 26 31 syld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐷 ) → ( ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 → ( 𝑎 + 𝑏 ) ∈ 𝐴 ) )
33 32 impancom ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) → ( 𝑏 ∈ 𝐷 → ( 𝑎 + 𝑏 ) ∈ 𝐴 ) )
34 5 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷 ) → ( ( 𝑎 + 𝑏 ) = ( 𝑎 + 𝑐 ) ↔ 𝑏 = 𝑐 ) ) )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) → ( ( 𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷 ) → ( ( 𝑎 + 𝑏 ) = ( 𝑎 + 𝑐 ) ↔ 𝑏 = 𝑐 ) ) )
36 33 35 dom2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) → ( 𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴 ) )
37 21 36 mpd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) ∧ ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 ) → 𝐷 ≼ 𝐴 )
38 20 37 mtand ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ¬ ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 )
39 dfrex2 ⊢ ( ∃ 𝑑 ∈ 𝐷 ( 𝑎 + 𝑑 ) ∈ 𝐵 ↔ ¬ ∀ 𝑑 ∈ 𝐷 ¬ ( 𝑎 + 𝑑 ) ∈ 𝐵 )
40 38 39 sylibr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ∃ 𝑑 ∈ 𝐷 ( 𝑎 + 𝑑 ) ∈ 𝐵 )
41 19 40 reximddv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ∃ 𝑑 ∈ 𝐷 ∃ 𝑦 ∈ 𝐵 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = 𝑦 ) )
42 vex ⊢ 𝑑 ∈ V
43 vex ⊢ 𝑦 ∈ V
44 42 43 op1std ⊢ ( 𝑥 = ⟨ 𝑑 , 𝑦 ⟩ → ( 1st ‘ 𝑥 ) = 𝑑 )
45 44 oveq2d ⊢ ( 𝑥 = ⟨ 𝑑 , 𝑦 ⟩ → ( 𝑐 + ( 1st ‘ 𝑥 ) ) = ( 𝑐 + 𝑑 ) )
46 42 43 op2ndd ⊢ ( 𝑥 = ⟨ 𝑑 , 𝑦 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑦 )
47 45 46 eqeq12d ⊢ ( 𝑥 = ⟨ 𝑑 , 𝑦 ⟩ → ( ( 𝑐 + ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) ↔ ( 𝑐 + 𝑑 ) = 𝑦 ) )
48 47 riotabidv ⊢ ( 𝑥 = ⟨ 𝑑 , 𝑦 ⟩ → ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) ) = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = 𝑦 ) )
49 48 eqeq2d ⊢ ( 𝑥 = ⟨ 𝑑 , 𝑦 ⟩ → ( 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) ) ↔ 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = 𝑦 ) ) )
50 49 rexxp ⊢ ( ∃ 𝑥 ∈ ( 𝐷 × 𝐵 ) 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) ) ↔ ∃ 𝑑 ∈ 𝐷 ∃ 𝑦 ∈ 𝐵 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + 𝑑 ) = 𝑦 ) )
51 41 50 sylibr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ∃ 𝑥 ∈ ( 𝐷 × 𝐵 ) 𝑎 = ( ℩ 𝑐 ∈ 𝐶 ( 𝑐 + ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) ) )
52 8 51 wdomd ⊢ ( 𝜑 → 𝐶 ≼* ( 𝐷 × 𝐵 ) )